Add a -max-sizet-in-bits option to our tools to control max size of address space
This allows one to shrink the size of counterexamples
MODIFY
llvm_util/cmd_args_def.h
llvm_util/cmd_args_def.h
@@ -20,6 +20,7 @@ smt::solver_print_queries(opt_smt_verbose);
smt::solver_tactic_verbose(opt_tactic_verbose);
config::debug = opt_debug;
config::max_offset_bits = opt_max_offset_in_bits;
+config::max_sizet_bits = opt_max_sizet_in_bits;
func_names.insert(opt_funcs.begin(), opt_funcs.end());

MODIFY
llvm_util/cmd_args_list.h
llvm_util/cmd_args_list.h
@@ -141,4 +141,11 @@ llvm::cl::opt<unsigned> opt_max_offset_in_bits(
"offset computations exceed the maximum."),
llvm::cl::cat(alive_cmdargs));
+llvm::cl::opt<unsigned> opt_max_sizet_in_bits(
+ LLVM_ARGS_PREFIX "max-sizet-in-bits", llvm::cl::init(64),
+ llvm::cl::desc("Upper bound for the size of size_t. "
+ "Note that this may impact correctness if the required "
+ "address space size exceeds the specified limit."),
+ llvm::cl::cat(alive_cmdargs));
+
}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -1038,6 +1038,7 @@ static void calculateAndInitConstants(Transform &t) {
// We need this assumption to support negative offsets.
bits_size_t = bit_width(max_alloc_size);
bits_size_t = min(max(bits_for_offset, bits_size_t), bits_program_pointer-1);
+ bits_size_t = min(bits_size_t, config::max_sizet_bits);
// +1 because the pointer after the object must be valid (can't overflow)
uint64_t loc_alloc_aligned_size

MODIFY
util/config.cpp
util/config.cpp
@@ -19,6 +19,7 @@ bool debug = false;
unsigned src_unroll_cnt = 0;
unsigned tgt_unroll_cnt = 0;
unsigned max_offset_bits = 64;
+unsigned max_sizet_bits = 64;
ostream &dbg() {
return *debug_os;

MODIFY
util/config.h
util/config.h
@@ -12,7 +12,7 @@ extern bool symexec_print_each_value;
extern bool skip_smt;
-// don't dumo if empty
+// don't dump if empty
extern std::string smt_benchmark_dir;
extern bool disable_poison_input;
@@ -30,6 +30,10 @@ extern unsigned tgt_unroll_cnt;
// maximum.
extern unsigned max_offset_bits;
+// Max bits for size_t. This limits the internal address space, like max block
+// size and size of pointers (not to be confused with program pointer size).
+extern unsigned max_sizet_bits;
+
std::ostream &dbg();
void set_debug(std::ostream &os);

Add a -max-sizet-in-bits option to our tools to control max size of address space
This allows one to shrink the size of counterexamples