add cmd arg options to configure max memory usage
MODIFY
smt/smt.cpp
smt/smt.cpp
@@ -48,9 +48,12 @@ const char* get_query_timeout() {
}
-// FIXME make this configurable
static uint64_t z3_memory_limit = 1ull << 30; // 1 GB
+void set_memory_limit(uint64_t limit) {
+ z3_memory_limit = limit;
+}
+
bool hit_memory_limit() {
return Z3_get_estimated_alloc_size() >= z3_memory_limit;
}

MODIFY
smt/smt.h
smt/smt.h
@@ -21,6 +21,7 @@ private:
void set_query_timeout(std::string ms);
const char* get_query_timeout();
+void set_memory_limit(uint64_t limit);
bool hit_memory_limit();
bool hit_half_memory_limit();

MODIFY
tools/alive.cpp
tools/alive.cpp
#include "tools/alive_parser.h"
#include "util/config.h"
#include "util/file.h"
+#include <cstdlib>
#include <iostream>
#include <string_view>
#include <vector>
@@ -25,6 +26,7 @@ static void show_help() {
" -v\t\tVerbose mode\n"
" -smt-stats\tShow SMT statistics\n"
" -smt-to:x\tTimeout for SMT queries in ms\n"
+ " -max-mem:x\tMax memory consumption in MB (aprox)\n"
" -smt-verbose\tPrint all SMT queries\n"
" -skip-smt\tSkip all SMT queries\n"
" -h / --help\tShow this help\n";
@@ -51,6 +53,9 @@ int main(int argc, char **argv) {
show_smt_stats = true;
else if (arg.compare(0, 8, "-smt-to:") == 0 && arg.size() > 8)
smt::set_query_timeout(arg.substr(8).data());
+ else if (arg.compare(0, 9, "-max-mem:") == 0 && arg.size() > 9)
+ smt::set_memory_limit(strtoul(arg.substr(9).data(), nullptr, 10) *
+ 1024 * 1024);
else if (arg == "-smt-verbose")
smt::solver_print_queries(true);
else if (arg == "-tactic-verbose")

MODIFY
tv/tv.cpp
tv/tv.cpp
@@ -36,6 +36,10 @@ llvm::cl::opt<unsigned> opt_smt_to(
"tv-smt-to", llvm::cl::desc("Alive: timeout for SMT queries"),
llvm::cl::init(1000), llvm::cl::value_desc("ms"));
+llvm::cl::opt<unsigned> opt_max_mem(
+ "tv-max-mem", llvm::cl::desc("Alive: max memory (aprox)"),
+ llvm::cl::init(1024), llvm::cl::value_desc("MB"));
+
llvm::cl::opt<bool> opt_se_verbose(
"tv-se-verbose", llvm::cl::desc("Alive: symbolic execution verbose mode"),
llvm::cl::init(false));
@@ -575,6 +579,7 @@ struct TVPass : public llvm::FunctionPass {
smt::solver_print_queries(opt_smt_verbose);
smt::solver_tactic_verbose(opt_tactic_verbose);
smt::set_query_timeout(to_string(opt_smt_to));
+ smt::set_memory_limit(opt_max_mem * 1024 * 1024);
config::skip_smt = opt_smt_skip;
config::symexec_print_each_value = opt_se_verbose;

add cmd arg options to configure max memory usage