unconditionally check for source functions that are UB for all execut…

…ions, but don't error out (#991)

llvm_util/cmd_args_def.h

@@ -11,7 +11,7 @@ config::src_unroll_cnt = opt_unrolling_factor;
 config::disable_undef_input = opt_disable_undef;
 config::disable_poison_input = opt_disable_poison;
 config::tgt_is_asm = opt_tgt_is_asm;
-config::check_if_src_is_ub = opt_check_if_src_is_ub;
+config::fail_if_src_is_ub = opt_fail_if_src_is_ub;
 config::symexec_print_each_value = opt_se_verbose;
 smt::set_query_timeout(to_string(opt_smt_to));
 smt::set_memory_limit((uint64_t)opt_smt_max_mem * 1024 * 1024);

llvm_util/cmd_args_list.h

@@ -40,9 +40,9 @@ llvm::cl::opt<bool> opt_disable_poison(LLVM_ARGS_PREFIX "disable-poison-input",
   llvm::cl::desc("Assume inputs are not poison (default=false)"),
   llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));
 
-llvm::cl::opt<bool> opt_check_if_src_is_ub(
-  LLVM_ARGS_PREFIX "check-src-ub",
-  llvm::cl::desc("Check if source function is always UB (default=false)"),
+llvm::cl::opt<bool> opt_fail_if_src_is_ub(
+  LLVM_ARGS_PREFIX "fail-src-ub",
+  llvm::cl::desc("Fail if source function is always UB (default=false)"),
   llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));
 
 llvm::cl::opt<bool> opt_tgt_is_asm(

tools/transform.cpp

@@ -502,10 +502,17 @@ check_refinement(Errors &errs, const Transform &t, State &src_state,
     axioms_expr = std::move(axioms)();
   }
 
-  if (config::check_if_src_is_ub &&
-      check_expr(axioms_expr && fndom_a).isUnsat()) {
-    errs.add("Source function is always UB", false);
-    return;
+  if (check_expr(axioms_expr && fndom_a).isUnsat()) {
+    cout << "\n"
+      "****************************************\n"
+      "WARNING: Source function is always UB.\n"
+      "It can be refined by any target function.\n"
+      "Please make sure this is what you wanted.\n"
+      "****************************************\n\n";
+    if (config::fail_if_src_is_ub) {
+      errs.add("Source function is always UB", false);
+      return;
+    }
   }
 
   {

util/config.cpp

@@ -16,7 +16,7 @@ string smt_benchmark_dir;
 bool disable_poison_input = false;
 bool disable_undef_input = false;
 bool tgt_is_asm = false;
-bool check_if_src_is_ub = false;
+bool fail_if_src_is_ub = false;
 bool disallow_ub_exploitation = false;
 bool debug = false;
 unsigned src_unroll_cnt = 0;

util/config.h

@@ -21,7 +21,7 @@ extern bool disable_undef_input;
 
 extern bool tgt_is_asm;
 
-extern bool check_if_src_is_ub;
+extern bool fail_if_src_is_ub;
 
 /// This is a special mode to verify that LLVM's optimizations are not
 /// exploiting UB. In particular, we disallow any UB related with arithmetic,