Skip to content

Commit d3b8719

Browse files
Tantalus13A98B5Fsonglinj-purdueKraks
authored
LMS linker (#6)
* draft: generate library * let's generate something * attempts * generate all library funcs * merge fix * scaffolding initlib * complete ImpCPSLLSC_lib * add output manifest * optimize initlib compilation * fix libc llsc posix codegen * take optional libPath * prepare for application gen * add more to ModDef * building application * app_main mangling * fix monitor generation * compilation passed for echo * a little refact * clean up * bugfix * bugfix & compile main file first * fix threadpool initialization error * bugfix * bugfix * fixup library code renaming * fix polyfill * minor changes * fix strange performance degradation * at/update simpl. version renamed * patch pure renaming * comments * add test case Co-authored-by: Songlin <[email protected]> Co-authored-by: Guannan Wei <[email protected]>
1 parent 7615cd3 commit d3b8719

20 files changed

+454
-84
lines changed

‎benchmarks/external-lib/link_app.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
extern int bar;
2+
3+
int foo();
4+
5+
int main(int argc, char** argv) {
6+
gs_assert_eager(bar == 10);
7+
gs_assert_eager(foo() == 1);
8+
return 0;
9+
}

‎benchmarks/external-lib/link_lib.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
int app_main(int argc, char** argv);
2+
3+
int bar;
4+
5+
int foo() {
6+
return 1;
7+
}
8+
9+
int main(int argc, char** argv) {
10+
bar = 10;
11+
return app_main(argc, argv);
12+
}

‎benchmarks/perf-mon/dataprocess.ipynb

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,8 @@
4848
"source": [
4949
"df['commit'] = pd.Categorical(df['commit'], df['commit'].unique(), ordered=True)\n",
5050
"df['para'] = pd.Categorical(df['para'], ['serial', 'par2', 'par4', 'par8', 'par16'], ordered=True)\n",
51-
"df['engine'] = pd.Categorical(df['engine'], ['ImpLLSC', 'ImpCPSLLSC', 'PureLLSC', 'PureCPSLLSC', 'PureCPSLLSC_Z3'], ordered=True)"
51+
"df['engine'] = pd.Categorical(df['engine'].str.replace('LLSC', 'GS'),\n",
52+
" ['ImpGS', 'ImpCPSGS', 'PureGS', 'PureCPSGS', 'PureCPSGS_Z3'], ordered=True)"
5253
]
5354
},
5455
{
@@ -84,7 +85,7 @@
8485
" ax = sns.violinplot(x='commit', y='wholeTime', hue='engine', data=data, ax=axes[1], **vio_styles)\n",
8586
" ax.set_title('%s - serial' % name)\n",
8687
" \n",
87-
" data = case[case['engine'] == \"PureCPSLLSC_Z3\"]\n",
88+
" data = case[case['para'] != \"serial\"]\n",
8889
" ax = sns.violinplot(x='commit', y='wholeTime', hue='para', data=data, ax=axes[2], **vio_styles)\n",
8990
" ax.set_title('%s - parallel' % name)"
9091
]

‎build.sbt

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,16 @@ scalacOptions ++= Seq(
3131

3232
autoCompilerPlugins := true
3333

34+
//https://www.scala-sbt.org/release/docs/Running-Project-Code.html
35+
fork := true
36+
run / javaOptions ++= Seq(
37+
"-Xms4G",
38+
"-Xmx32G",
39+
"-Xss1024M",
40+
"-XX:MaxMetaspaceSize=8G",
41+
"-XX:ReservedCodeCacheSize=2048M"
42+
)
43+
3444
val paradiseVersion = "2.1.0"
3545
addCompilerPlugin("org.scalamacros" % "paradise" % paradiseVersion cross CrossVersion.full)
3646
addCompilerPlugin("org.typelevel" %% "kind-projector" % "0.11.3" cross CrossVersion.full)

‎headers/gensym/external_imp.hpp

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ inline T __make_symbolic(SS& state, List<PtrVal>& args, __Cont<T> k) {
7474
state.add_symbolic(object_name, len, false);
7575
//std::cout << "sym array size: " << proj_LocV_size(loc) << "\n";
7676
for (int i = 0; i < len; i++) {
77-
state.update(loc + i, make_SymV(object_name + "_" + std::to_string(i), 8));
77+
state.update_simpl(loc + i, make_SymV(object_name + "_" + std::to_string(i), 8));
7878
}
7979
return k(state, make_IntV(0));
8080
}
@@ -221,7 +221,7 @@ inline T __realloc(SS& state, List<PtrVal>& args, __Cont<T> k) {
221221
Addr src = proj_LocV(args.at(0));
222222
IntData prevBytes = proj_LocV_size(args.at(0));
223223
for (int i = 0; i < prevBytes; i++) {
224-
state.update(memLoc + i, state.heap_lookup(src + i));
224+
state.update_simpl(memLoc + i, state.heap_lookup(src + i));
225225
}
226226
}
227227
return k(state, memLoc);
@@ -249,7 +249,7 @@ inline T __reallocarray(SS& state, List<PtrVal>& args, __Cont<T> k) {
249249
Addr src = proj_LocV(args.at(0));
250250
IntData prevBytes = proj_LocV_size(args.at(0));
251251
for (int i = 0; i < prevBytes; i++) {
252-
state.update(memLoc + i, state.heap_lookup(src + i));
252+
state.update_simpl(memLoc + i, state.heap_lookup(src + i));
253253
}
254254
}
255255
return k(state, memLoc);
@@ -290,7 +290,7 @@ inline T __llvm_memcpy(SS& state, List<PtrVal>& args, __Cont<T> k) {
290290
ASSERT(std::dynamic_pointer_cast<LocV>(dest) != nullptr, "Non-location value");
291291
ASSERT(std::dynamic_pointer_cast<LocV>(src) != nullptr, "Non-location value");
292292
for (int i = 0; i < bytes_int; i++) {
293-
state.update(dest + i, state.at(src + i));
293+
state.update_simpl(dest + i, state.at_simpl(src + i));
294294
}
295295
return k(state, IntV0_32);
296296
}
@@ -314,10 +314,10 @@ inline T __llvm_memmove(SS& state, List<PtrVal>& args, __Cont<T> k) {
314314
IntData bytes_int = proj_IntV(args.at(2));
315315
auto temp_mem = TrList<PtrVal>{};
316316
for (int i = 0; i < bytes_int; i++) {
317-
temp_mem.push_back(state.at(src + i));
317+
temp_mem.push_back(state.at_simpl(src + i));
318318
}
319319
for (int i = 0; i < bytes_int; i++) {
320-
state.update(dest + i, temp_mem.at(i));
320+
state.update_simpl(dest + i, temp_mem.at(i));
321321
}
322322
return k(state, IntV0_32);
323323
}
@@ -339,7 +339,7 @@ inline T __llvm_memset(SS& state, List<PtrVal>& args, __Cont<T> k) {
339339
ASSERT(std::dynamic_pointer_cast<LocV>(dest) != nullptr, "Non-location value");
340340
auto v = make_IntV(0, 8);
341341
for (int i = 0; i < bytes_int; i++) {
342-
state.update(dest + i, v);
342+
state.update_simpl(dest + i, v);
343343
}
344344
return k(state, IntV0_32);
345345
}
@@ -355,7 +355,7 @@ inline std::monostate llvm_memset(SS& state, List<PtrVal> args, Cont k) {
355355
inline void copy_native2state(SS& state, PtrVal ptr, char* buf, int size) {
356356
ASSERT(buf && size > 0, "Invalid native buffer");
357357
for (int i = 0; i < size; ) {
358-
auto old_val = state.at(ptr + i);
358+
auto old_val = state.at_simpl(ptr + i);
359359
if (old_val) {
360360
if (std::dynamic_pointer_cast<ShadowV>(old_val) || std::dynamic_pointer_cast<LocV>(old_val)) {
361361
ABORT("unhandled ptrval: shadowv && LocV");
@@ -367,13 +367,13 @@ inline void copy_native2state(SS& state, PtrVal ptr, char* buf, int size) {
367367
i = i + bytes_num;
368368
} else {
369369
for (int j = 0; j < bytes_num; j++) {
370-
state.update(ptr + i, make_IntV(buf[i], 8));
370+
state.update_simpl(ptr + i, make_IntV(buf[i], 8));
371371
i++;
372372
if (i >= size) break;
373373
}
374374
}
375375
} else {
376-
state.update(ptr + i, make_IntV(buf[i], 8));
376+
state.update_simpl(ptr + i, make_IntV(buf[i], 8));
377377
i++;
378378
}
379379
}

‎headers/gensym/external_pure.hpp

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ inline T __make_symbolic(SS& state, List<PtrVal>& args, __Cont<T> k) {
6666
SS res = state.add_symbolic(object_name, len, false);
6767
//std::cout << "sym array size: " << proj_LocV_size(loc) << "\n";
6868
for (int i = 0; i < len; i++) {
69-
res = res.update(loc + i, make_SymV(object_name + "_" + std::to_string(i), 8));
69+
res = res.update_simpl(loc + i, make_SymV(object_name + "_" + std::to_string(i), 8));
7070
}
7171
return k(res, make_IntV(0));
7272
}
@@ -189,7 +189,7 @@ inline T __realloc(SS& state, List<PtrVal>& args, __Cont<T> k) {
189189
Addr src = proj_LocV(args.at(0));
190190
IntData prevBytes = proj_LocV_size(args.at(0));
191191
for (int i = 0; i < prevBytes; i++) {
192-
res = res.update(memLoc + i, res.heap_lookup(src + i));
192+
res = res.update_simpl(memLoc + i, res.heap_lookup(src + i));
193193
}
194194
}
195195
return k(res, memLoc);
@@ -218,7 +218,7 @@ inline T __reallocarray(SS& state, List<PtrVal>& args, __Cont<T> k) {
218218
Addr src = proj_LocV(args.at(0));
219219
IntData prevBytes = proj_LocV_size(args.at(0));
220220
for (int i = 0; i < prevBytes; i++) {
221-
res = res.update(memLoc + i, res.heap_lookup(src + i));
221+
res = res.update_simpl(memLoc + i, res.heap_lookup(src + i));
222222
}
223223
}
224224
return k(res, memLoc);
@@ -284,7 +284,7 @@ inline T __llvm_memcpy(SS& state, List<PtrVal>& args, __Cont<T> k) {
284284
ASSERT(std::dynamic_pointer_cast<LocV>(src) != nullptr, "Non-location value");
285285
SS res = state;
286286
for (int i = 0; i < bytes_int; i++) {
287-
res = res.update(dest + i, res.at(src + i));
287+
res = res.update_simpl(dest + i, res.at_simpl(src + i));
288288
}
289289
return k(res, IntV0_32);
290290
}
@@ -309,10 +309,10 @@ inline T __llvm_memmove(SS& state, List<PtrVal>& args, __Cont<T> k) {
309309
IntData bytes_int = proj_IntV(args.at(2));
310310
auto temp_mem = TrList<PtrVal>{};
311311
for (int i = 0; i < bytes_int; i++) {
312-
temp_mem.push_back(res.at(src + i));
312+
temp_mem.push_back(res.at_simpl(src + i));
313313
}
314314
for (int i = 0; i < bytes_int; i++) {
315-
res = res.update(dest + i, temp_mem.at(i));
315+
res = res.update_simpl(dest + i, temp_mem.at(i));
316316
}
317317
return k(res, IntV0_32);
318318
}
@@ -335,7 +335,7 @@ inline T __llvm_memset(SS& state, List<PtrVal>& args, __Cont<T> k) {
335335
auto v = make_IntV(0, 8);
336336
SS res = state;
337337
for (int i = 0; i < bytes_int; i++) {
338-
res = res.update(dest + i, v);
338+
res = res.update_simpl(dest + i, v);
339339
}
340340
return k(res, IntV0_32);
341341
}
@@ -354,7 +354,7 @@ inline SS copy_native2state(SS state, PtrVal ptr, char* buf, int size) {
354354
ASSERT(buf && size > 0, "Invalid native buffer");
355355
SS res = state;
356356
for (int i = 0; i < size; ) {
357-
auto old_val = state.at(ptr + i);
357+
auto old_val = state.at_simpl(ptr + i);
358358
if (old_val) {
359359
if (std::dynamic_pointer_cast<ShadowV>(old_val) || std::dynamic_pointer_cast<LocV>(old_val)) {
360360
ABORT("unhandled ptrval: shadowv && LocV");
@@ -367,13 +367,13 @@ inline SS copy_native2state(SS state, PtrVal ptr, char* buf, int size) {
367367
i = i + bytes_num;
368368
} else {
369369
for (int j = 0; j < bytes_num; j++) {
370-
res = res.update(ptr + i, make_IntV(buf[i], 8));
370+
res = res.update_simpl(ptr + i, make_IntV(buf[i], 8));
371371
i++;
372372
if (i >= size) break;
373373
}
374374
}
375375
} else {
376-
res = res.update(ptr + i, make_IntV(buf[i], 8));
376+
res = res.update_simpl(ptr + i, make_IntV(buf[i], 8));
377377
i++;
378378
}
379379
}

‎headers/gensym/external_shared.hpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -113,12 +113,12 @@ inline List<PtrVal> get_sym_string_at(SS& state, PtrVal ptr) {
113113
TrList<PtrVal> name;
114114
PtrVal v;
115115
ASSERT(std::dynamic_pointer_cast<LocV>(ptr) != nullptr, "Non-location value");
116-
v = state.at(ptr);
116+
v = state.at_simpl(ptr);
117117
while (!(v->is_conc() && proj_IntV_char(v) == '\0')) {
118118
INFO("get_sym_string: v=" << v->toString() << " at " << ptr->toString());
119119
name.push_back(v);
120120
ptr = ptr + 1;
121-
v = state.at(ptr);
121+
v = state.at_simpl(ptr);
122122
}
123123
return name.persistent();
124124
}
@@ -149,20 +149,20 @@ inline double get_float_arg(SS& state, PtrVal x) {
149149

150150
inline std::string get_string_arg(SS& state, PtrVal ptr) {
151151
std::string name;
152-
char c = get_int_arg(state, state.at(ptr)); // c = *ptr
152+
char c = get_int_arg(state, state.at_simpl(ptr)); // c = *ptr
153153
ASSERT(std::dynamic_pointer_cast<LocV>(ptr) != nullptr, "Non-location value");
154154
while (c != '\0') {
155155
name += c;
156156
ptr = ptr + 1;
157-
c = get_int_arg(state, state.at(ptr)); // c = *ptr
157+
c = get_int_arg(state, state.at_simpl(ptr)); // c = *ptr
158158
}
159159
return name;
160160
}
161161

162162
inline void copy_state2native(SS& state, PtrVal ptr, char* buf, int size) {
163163
ASSERT(buf && size > 0, "Invalid native buffer");
164164
for (int i = 0; i < size; ) {
165-
auto val = state.at(ptr + i);
165+
auto val = state.at_simpl(ptr + i);
166166
if (val) {
167167
if (std::dynamic_pointer_cast<ShadowV>(val) || std::dynamic_pointer_cast<LocV>(val)) {
168168
ABORT("unhandled ptrval: shadowv && LocV");

‎headers/gensym/libcpolyfill.hpp

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// prepare necessary declarations and definitions for library mode compilation
2+
#include <gensym.hpp>
3+
std::monostate app_main(SS&, immer::flex_vector<PtrVal>, std::function<std::monostate(SS&, PtrVal)>);
4+
std::monostate gs_main(SS&, immer::flex_vector<PtrVal>, std::function<std::monostate(SS&, PtrVal)>);
5+
inline std::monostate gs_dummy(SS&, immer::flex_vector<PtrVal>, std::function<std::monostate(SS&, PtrVal)>) {
6+
return std::monostate{};
7+
}
8+
inline std::monostate start_gs_main(SS& state, immer::flex_vector<PtrVal> args, std::function<std::monostate(SS&, PtrVal)> cont) {
9+
if (can_par_tp()) {
10+
tp.add_task(1, [=] () mutable { return gs_main(state, args, cont); });
11+
return std::monostate{};
12+
}
13+
return gs_main(state, args, cont);
14+
}

‎headers/gensym/monitor.hpp

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,10 +26,15 @@ struct Monitor {
2626

2727
public:
2828
Monitor() : num_blocks(0), num_paths(0), num_states(1), start(steady_clock::now()) {}
29-
Monitor(uint64_t num_blocks, std::vector<std::pair<unsigned, unsigned>> branch_num) :
29+
Monitor(uint64_t num_blocks, const std::vector<std::pair<unsigned, unsigned>> &branch_num) :
3030
num_blocks(num_blocks), num_paths(0), num_states(1),
3131
block_cov(num_blocks),
3232
start(steady_clock::now()) {
33+
extend_blocks(num_blocks, branch_num);
34+
}
35+
36+
void extend_blocks(uint64_t nblks, const std::vector<std::pair<unsigned, unsigned>> &branch_num) {
37+
if (num_blocks != nblks) block_cov = std::move(decltype(block_cov)(num_blocks = nblks));
3338
// `branch_num` contains the ids of blocks whose terminator is br/switch,
3439
// for each of such block, `br_arity` is the number of branches.
3540
for (const auto& [blk_id, br_arity] : branch_num) {

‎headers/gensym/state_pure.hpp

Lines changed: 19 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -481,7 +481,13 @@ class SS: public Printable {
481481
// Todo: should we modify the pc to add the in-bound constraints
482482
return read_res;
483483
}
484-
PtrVal at(const PtrVal& addr, size_t size = 1) {
484+
PtrVal at_simpl(const PtrVal& addr) {
485+
auto loc = std::dynamic_pointer_cast<LocV>(addr);
486+
ASSERT(loc != nullptr, "Lookup an non-address value");
487+
if (loc->k == LocV::kStack) return stack.at(loc->l);
488+
return heap.at(loc->l);
489+
}
490+
PtrVal at(const PtrVal& addr, size_t size) {
485491
auto loc = std::dynamic_pointer_cast<LocV>(addr);
486492
if (loc != nullptr) {
487493
if (loc->k == LocV::kStack) return stack.at(loc->l, size);
@@ -523,7 +529,13 @@ class SS: public Printable {
523529
List<PtrVal> get_preferred_cex() { return meta.preferred_cex; }
524530
SS alloc_stack(size_t size) { return SS(heap, stack.alloc(size), pc, meta, fs); }
525531
SS alloc_heap(size_t size) { return SS(heap.alloc(size), stack, pc, meta, fs); }
526-
SS update(const PtrVal& addr, const PtrVal& val, size_t size = 1) {
532+
SS update_simpl(const PtrVal& addr, const PtrVal& val) {
533+
auto loc = std::dynamic_pointer_cast<LocV>(addr);
534+
ASSERT(loc != nullptr, "Lookup an non-address value");
535+
if (loc->k == LocV::kStack) return SS(heap, stack.update(loc->l, val), pc, meta, fs);
536+
return SS(heap.update(loc->l, val), stack, pc, meta, fs);
537+
}
538+
SS update(const PtrVal& addr, const PtrVal& val, size_t size) {
527539
auto loc = std::dynamic_pointer_cast<LocV>(addr);
528540
ASSERT(loc != nullptr, "Lookup an non-address value");
529541
if (loc->k == LocV::kStack) return SS(heap, stack.update(loc->l, val, size), pc, meta, fs);
@@ -532,7 +544,7 @@ class SS: public Printable {
532544
SS update_seq(PtrVal addr, List<PtrVal> vals) {
533545
SS updated_ss = *this;
534546
for (int i = 0; i < vals.size(); i++) {
535-
updated_ss = updated_ss.update(addr + i, vals.at(i));
547+
updated_ss = updated_ss.update_simpl(addr + i, vals.at(i));
536548
}
537549
return updated_ss;
538550
}
@@ -575,11 +587,11 @@ class SS: public Printable {
575587
auto arg_ptr = make_LocV(updated_ss.stack_size(), LocV::kStack, arg.size(), 0); // top of the stack
576588
updated_ss = updated_ss.alloc_stack(arg.size());
577589
updated_ss = updated_ss.update_seq(arg_ptr, arg); // copy the values to the newly allocated space
578-
updated_ss = updated_ss.update(stack_ptr + (8 * i), arg_ptr); // copy the pointer value
590+
updated_ss = updated_ss.update_simpl(stack_ptr + (8 * i), arg_ptr); // copy the pointer value
579591
}
580-
updated_ss = updated_ss.update(stack_ptr + (8 * num_args), make_LocV_null()); // terminate the array of pointers
581-
updated_ss = updated_ss.update(stack_ptr + (8 * (num_args + 1)), make_LocV_null()); // terminate the empty envp array
582-
updated_ss = updated_ss.update(stack_ptr + (8 * (num_args + 2)), make_LocV_null()); // additional terminating null that uclibc seems to expect for the ELF header
592+
updated_ss = updated_ss.update_simpl(stack_ptr + (8 * num_args), make_LocV_null()); // terminate the array of pointers
593+
updated_ss = updated_ss.update_simpl(stack_ptr + (8 * (num_args + 1)), make_LocV_null()); // terminate the empty envp array
594+
updated_ss = updated_ss.update_simpl(stack_ptr + (8 * (num_args + 2)), make_LocV_null()); // additional terminating null that uclibc seems to expect for the ELF header
583595

584596
return updated_ss;
585597
}

0 commit comments

Comments
 (0)