fix(runtime): replace lean::alloca with macro

Functions using `alloca` are not inlined even when marked with
`inline` in some compilers.

Remark: GCC will _not_ inline a function calling alloca unless it is
annotated with always_inline.
This commit is contained in:
Leonardo de Moura 2019-02-04 09:36:53 -08:00
parent b4a78a0280
commit 98edae152a
3 changed files with 43 additions and 51 deletions

View file

@ -74,7 +74,7 @@ do emit $ sformat! "obj* apply_{n}(obj* f, {arg_decls}) {{\n",
emit " default:\n",
emit $ sformat! " lean_assert(arity > {max});\n",
emit $ sformat! " obj * as[{n}] = {{ {args} };\n",
emit " obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT\n",
emit " obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT\n",
emit " for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }\n",
emit $ sformat! " for (unsigned i = 0; i < {n}; i++) args[fixed+i] = as[i];\n",
emit " obj * r = FNN(f)(args);\n",
@ -84,7 +84,7 @@ do emit $ sformat! "obj* apply_{n}(obj* f, {arg_decls}) {{\n",
emit $ sformat! "} else if (arity < fixed + {n}) {{\n",
if n ≥ 2 then do
emit $ sformat! " obj * as[{n}] = {{ {args} };\n",
emit " obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT\n",
emit " obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT\n",
emit " for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }\n",
emit " for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];\n",
emit " obj * new_f = curry(f, arity, args);\n",
@ -124,14 +124,14 @@ do emit "obj* apply_m(obj* f, unsigned n, obj** as) {\n",
emit "unsigned arity = closure_arity(f);\n",
emit "unsigned fixed = closure_num_fixed(f);\n",
emit $ sformat! "if (arity == fixed + n) {{\n",
emit " obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT\n",
emit " obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT\n",
emit " for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }\n",
emit " for (unsigned i = 0; i < n; i++) args[fixed+i] = as[i];\n",
emit " obj * r = FNN(f)(args);\n",
emit " dec_ref(f);\n",
emit " return r;\n",
emit $ sformat! "} else if (arity < fixed + n) {{\n",
emit " obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT\n",
emit " obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT\n",
emit " for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }\n",
emit " for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];\n",
emit " obj * new_f = FNN(f)(args);\n",

View file

@ -141,7 +141,7 @@ if (arity == fixed + 1) {
default:
lean_assert(arity > 16);
obj * as[1] = { a1 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 1; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -197,7 +197,7 @@ if (arity == fixed + 2) {
default:
lean_assert(arity > 16);
obj * as[2] = { a1, a2 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 2; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -206,7 +206,7 @@ if (arity == fixed + 2) {
}
} else if (arity < fixed + 2) {
obj * as[2] = { a1, a2 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -256,7 +256,7 @@ if (arity == fixed + 3) {
default:
lean_assert(arity > 16);
obj * as[3] = { a1, a2, a3 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 3; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -265,7 +265,7 @@ if (arity == fixed + 3) {
}
} else if (arity < fixed + 3) {
obj * as[3] = { a1, a2, a3 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -313,7 +313,7 @@ if (arity == fixed + 4) {
default:
lean_assert(arity > 16);
obj * as[4] = { a1, a2, a3, a4 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 4; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -322,7 +322,7 @@ if (arity == fixed + 4) {
}
} else if (arity < fixed + 4) {
obj * as[4] = { a1, a2, a3, a4 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -368,7 +368,7 @@ if (arity == fixed + 5) {
default:
lean_assert(arity > 16);
obj * as[5] = { a1, a2, a3, a4, a5 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 5; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -377,7 +377,7 @@ if (arity == fixed + 5) {
}
} else if (arity < fixed + 5) {
obj * as[5] = { a1, a2, a3, a4, a5 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -421,7 +421,7 @@ if (arity == fixed + 6) {
default:
lean_assert(arity > 16);
obj * as[6] = { a1, a2, a3, a4, a5, a6 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 6; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -430,7 +430,7 @@ if (arity == fixed + 6) {
}
} else if (arity < fixed + 6) {
obj * as[6] = { a1, a2, a3, a4, a5, a6 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -472,7 +472,7 @@ if (arity == fixed + 7) {
default:
lean_assert(arity > 16);
obj * as[7] = { a1, a2, a3, a4, a5, a6, a7 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 7; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -481,7 +481,7 @@ if (arity == fixed + 7) {
}
} else if (arity < fixed + 7) {
obj * as[7] = { a1, a2, a3, a4, a5, a6, a7 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -521,7 +521,7 @@ if (arity == fixed + 8) {
default:
lean_assert(arity > 16);
obj * as[8] = { a1, a2, a3, a4, a5, a6, a7, a8 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 8; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -530,7 +530,7 @@ if (arity == fixed + 8) {
}
} else if (arity < fixed + 8) {
obj * as[8] = { a1, a2, a3, a4, a5, a6, a7, a8 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -568,7 +568,7 @@ if (arity == fixed + 9) {
default:
lean_assert(arity > 16);
obj * as[9] = { a1, a2, a3, a4, a5, a6, a7, a8, a9 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 9; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -577,7 +577,7 @@ if (arity == fixed + 9) {
}
} else if (arity < fixed + 9) {
obj * as[9] = { a1, a2, a3, a4, a5, a6, a7, a8, a9 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -613,7 +613,7 @@ if (arity == fixed + 10) {
default:
lean_assert(arity > 16);
obj * as[10] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 10; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -622,7 +622,7 @@ if (arity == fixed + 10) {
}
} else if (arity < fixed + 10) {
obj * as[10] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -656,7 +656,7 @@ if (arity == fixed + 11) {
default:
lean_assert(arity > 16);
obj * as[11] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 11; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -665,7 +665,7 @@ if (arity == fixed + 11) {
}
} else if (arity < fixed + 11) {
obj * as[11] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -697,7 +697,7 @@ if (arity == fixed + 12) {
default:
lean_assert(arity > 16);
obj * as[12] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 12; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -706,7 +706,7 @@ if (arity == fixed + 12) {
}
} else if (arity < fixed + 12) {
obj * as[12] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -736,7 +736,7 @@ if (arity == fixed + 13) {
default:
lean_assert(arity > 16);
obj * as[13] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 13; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -745,7 +745,7 @@ if (arity == fixed + 13) {
}
} else if (arity < fixed + 13) {
obj * as[13] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -773,7 +773,7 @@ if (arity == fixed + 14) {
default:
lean_assert(arity > 16);
obj * as[14] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 14; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -782,7 +782,7 @@ if (arity == fixed + 14) {
}
} else if (arity < fixed + 14) {
obj * as[14] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -808,7 +808,7 @@ if (arity == fixed + 15) {
default:
lean_assert(arity > 16);
obj * as[15] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 15; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -817,7 +817,7 @@ if (arity == fixed + 15) {
}
} else if (arity < fixed + 15) {
obj * as[15] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -841,7 +841,7 @@ if (arity == fixed + 16) {
default:
lean_assert(arity > 16);
obj * as[16] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < 16; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
@ -850,7 +850,7 @@ if (arity == fixed + 16) {
}
} else if (arity < fixed + 16) {
obj * as[16] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16 };
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = curry(f, arity, args);
@ -865,14 +865,14 @@ lean_assert(n > 16);
unsigned arity = closure_arity(f);
unsigned fixed = closure_num_fixed(f);
if (arity == fixed + n) {
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < n; i++) args[fixed+i] = as[i];
obj * r = FNN(f)(args);
dec_ref(f);
return r;
} else if (arity < fixed + n) {
obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
obj * new_f = FNN(f)(args);

View file

@ -16,6 +16,12 @@ Author: Leonardo de Moura
#include "runtime/int64.h"
#include "runtime/thread.h"
#ifdef _MSC_VER
#define LEAN_ALLOCA(s) ::_alloca(s)
#else
#define LEAN_ALLOCA(s) ::alloca(s)
#endif
namespace lean {
typedef unsigned char uint8;
typedef unsigned short uint16;
@ -23,20 +29,6 @@ typedef unsigned uint32;
typedef unsigned long long uint64;
typedef size_t usize;
/*
The primitives implemented in the runtime do not modify the RC of its arguments.
Callers are responsible for increasing/decreasing the RCs using the `inc`/`dec` operations.
All new objects allocated by the primitives have RC == 1.
*/
inline void * alloca(size_t s) {
#ifdef _MSC_VER
return ::_alloca(s);
#else
return ::alloca(s);
#endif
}
/* Objects can be stored in 5 different kinds of memory:
- `MTHeap`: multi-threaded heap, the reference counter (RC) is updated using atomic operations.
All objects reachable from an object in the `MTHeap` are in `MTHeap`, `Persistent` or `Region`.