alive-tv: add -dbg flag, add CHECK: test to lit
ADD
tests/alive-tv/dbg.src.ll
+; TEST-ARGS: -dbg
+
+define i16 @test(i16) {
+ %v = add i16 %0, %0
+ ret i16 %v
+}
+
+; CHECK: num_locals: 0

ADD
tests/alive-tv/dbg.tgt.ll
+define i16 @test(i16) {
+ %v = add i16 %0, %0
+ ret i16 %v
+}

MODIFY
tests/lit/lit/formats/alive2test.py
tests/lit/lit/formats/alive2test.py
@@ -40,6 +40,7 @@ class Alive2Test(TestFormat):
self.regex_errs = re.compile(r";\s*(ERROR:.*)")
self.regex_xfail = re.compile(r";\s*XFAIL:\s*(.*)")
self.regex_args = re.compile(r";\s*TEST-ARGS:(.*)")
+ self.regex_check = re.compile(r";\s*CHECK:(.*)")
def getTestsInDirectory(self, testSuite, path_in_suite,
litConfig, localConfig):
@@ -97,6 +98,10 @@ class Alive2Test(TestFormat):
expect_err = self.regex_errs.search(input)
xfail = self.regex_xfail.search(input)
+ chk = self.regex_check.search(input)
+
+ if chk != None and (out + err).find(chk.group(1).strip()) == -1:
+ return lit.Test.FAIL, out + err
if expect_err is None and xfail is None:
if exitCode == 0 and string.find(out + err, ok_string) != -1:

MODIFY
tools/alive-tv.cpp
tools/alive-tv.cpp
@@ -60,6 +60,10 @@ static llvm::cl::opt<bool> opt_smt_verbose(
"smt-verbose", llvm::cl::desc("Alive: SMT verbose mode"),
llvm::cl::cat(opt_alive), llvm::cl::init(false));
+static llvm::cl::opt<bool> opt_debug(
+ "dbg", llvm::cl::desc("Alive: print debugging info"),
+ llvm::cl::cat(opt_alive), llvm::cl::init(false));
+
static llvm::cl::opt<bool> opt_smt_stats(
"smt-stats", llvm::cl::desc("Alive: show SMT statistics"),
llvm::cl::cat(opt_alive), llvm::cl::init(false));
@@ -281,6 +285,7 @@ int main(int argc, char **argv) {
config::symexec_print_each_value = opt_se_verbose;
config::disable_undef_input = opt_disable_undef;
config::disable_poison_input = opt_disable_poison;
+ config::debug = opt_debug;
auto M1 = openInputFile(Context, opt_file1);
if (!M1.get())

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -435,6 +435,18 @@ static void calculateAndInitConstants(Transform &t) {
bits_size_t = 64;
little_endian = t.src.isLittleEndian();
+
+ if (config::debug)
+ config::dbg() << "num_max_nonlocals_inst: " << num_max_nonlocals_inst << "\n"
+ "num_locals: " << num_locals << "\n"
+ "num_nonlocals: " << num_nonlocals << "\n"
+ "bits_for_bid: " << bits_for_bid << "\n"
+ "bits_for_offset: " << bits_for_offset << "\n"
+ "bits_size_t: " << bits_size_t << "\n"
+ "little_endian: " << little_endian << "\n"
+ "nullptr_is_used: " << nullptr_is_used << "\n"
+ "has_int2ptr: " << has_int2ptr << "\n"
+ "has_ptr2int: " << has_ptr2int << "\n";
}

MODIFY
util/config.cpp
util/config.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "util/config.h"
+#include <iostream>
+
+using namespace std;
+
+static ostream *debug_os = &cerr;
namespace util::config {
@@ -9,5 +14,14 @@ bool symexec_print_each_value = false;
bool skip_smt = false;
bool disable_poison_input = false;
bool disable_undef_input = false;
+bool debug = false;
+
+ostream &dbg() {
+ return *debug_os;
+}
+
+void set_debug(ostream &os) {
+ debug_os = &os;
+}
}

MODIFY
util/config.h
util/config.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+#include <ostream>
+
namespace util::config {
extern bool symexec_print_each_value;
@@ -13,4 +15,9 @@ extern bool disable_poison_input;
extern bool disable_undef_input;
+extern bool debug;
+
+std::ostream &dbg();
+void set_debug(std::ostream &os);
+
}

alive-tv: add -dbg flag, add CHECK: test to lit (#195)