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

Author: nunoplopes

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());
 

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));
+
 }

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

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;

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);