From 3702bfcb81d3ddd6dc1df633f8ea1f4f82862c3c Mon Sep 17 00:00:00 2001 From: Peter Goodman Date: Mon, 30 Oct 2017 14:16:02 -0400 Subject: [PATCH] Changed how the logging works to log to a static buffer, then the hooks pull info out from there. --- bin/mctest/__main__.py | 33 +++++++-------- bin/mctest/main_angr.py | 37 ++++++++++++----- examples/CMakeLists.txt | 2 +- .../{OutOfBoundsInt.c => OutOfBoundsInt.cpp} | 16 ++++---- src/include/mctest/McTest.h | 2 +- src/lib/McTest.c | 40 +++++++++++++++---- 6 files changed, 86 insertions(+), 44 deletions(-) rename examples/{OutOfBoundsInt.c => OutOfBoundsInt.cpp} (69%) diff --git a/bin/mctest/__main__.py b/bin/mctest/__main__.py index 92d3b17..7f65973 100644 --- a/bin/mctest/__main__.py +++ b/bin/mctest/__main__.py @@ -174,19 +174,20 @@ LEVEL_TO_LOGGER = { } -def hook_Log(state, level, begin_ea, end_ea): +def hook_Log(state, level, begin_ea): """Implements McTest_Log, which lets Manticore intercept and handle the printing of log messages from the simulated tests.""" level = state.solve_one(level) assert level in LEVEL_TO_LOGGER begin_ea = state.solve_one(begin_ea) - end_ea = state.solve_one(end_ea) - assert begin_ea <= end_ea message_bytes = [] - for i in xrange(end_ea - begin_ea): - message_bytes.append(state.cpu.memory[begin_ea + i]) + for i in xrange(4096): + b = state.cpu.read_int(begin_ea + i, 8) + if not issymbolic(b) and b == 0: + break + message_bytes.append(b) state.context['log_messages'].append((level, message_bytes)) @@ -209,14 +210,11 @@ def done_test(_, state, state_id, reason): for level, message_bytes in state.context['log_messages']: message = [] for b in message_bytes: - if issymbolic(b): - b_ord = state.solve_one(b) - state.constrain(b == b_ord) - message.append(chr(b_ord)) - elif isinstance(b, (int, long)): - message.append(chr(b)) + b_ord = state.solve_one(b) + if b_ord == 0: + break else: - message.append(b) + message.append(chr(b_ord)) LEVEL_TO_LOGGER[level]("".join(message)) @@ -230,8 +228,7 @@ def done_test(_, state, state_id, reason): output = [] for i in xrange(input_length): b = state.cpu.read_int(state.context['InputBegin'] + i, 8) - if issymbolic(b): - b = state.solve_one(b) + b = state.solve_one(b) output.append("{:2x}".format(b)) L.info("Input: {}".format(" ".join(output))) @@ -244,7 +241,7 @@ def do_run_test(state, apis, test): m.verbosity(1) state = m.initial_state - messages = [(1, "Running {} from {}:{}".format( + messages = [(1, "Running {} from {}({})".format( test.name, test.file_name, test.line_number))] state.context['InputBegin'] = apis['InputBegin'] @@ -279,6 +276,10 @@ def run_tests(args, state, apis): pool = multiprocessing.Pool(processes=max(1, args.num_workers)) results = [] tests = find_test_cases(state, apis['LastTestInfo']) + + L.info("Running {} tests across {} workers".format( + len(tests), args.num_workers)) + for test in tests: res = pool.apply_async(run_test, (state, apis, test)) results.append(res) @@ -302,7 +303,7 @@ def main(): args = parser.parse_args() - m = manticore.Manticore(sys.argv[1], sys.argv[1:]) + m = manticore.Manticore(args.binary) m.verbosity(1) # Hack to get around current broken _get_symbol_address diff --git a/bin/mctest/main_angr.py b/bin/mctest/main_angr.py index 33340a1..aec0a66 100644 --- a/bin/mctest/main_angr.py +++ b/bin/mctest/main_angr.py @@ -29,7 +29,7 @@ L.setLevel(logging.INFO) def hook_function(project, ea, cls): - """Hook the function `name` with the SimProcedure `cls`.""" + """Hook the function `ea` with the SimProcedure `cls`.""" project.hook(ea, cls(project=project)) @@ -186,16 +186,22 @@ LEVEL_TO_LOGGER = { class Log(angr.SimProcedure): """Implements McTest_Log, which lets Angr intercept and handle the printing of log messages from the simulated tests.""" - def run(self, level, begin_ea, end_ea): + def run(self, level, begin_ea_): level = self.state.solver.eval(level, cast_to=int) assert level in LEVEL_TO_LOGGER - begin_ea = self.state.solver.eval(begin_ea, cast_to=int) - end_ea = self.state.solver.eval(end_ea, cast_to=int) - assert begin_ea <= end_ea + begin_ea = self.state.solver.eval(begin_ea_, cast_to=int) + if self.state.se.symbolic(begin_ea_): + self.state.solver.add(begin_ea_ == begin_ea) + + data = [] + for i in xrange(4096): + b = self.state.memory.load(begin_ea + i, size=1) + solutions = self.state.solver.eval_upto(b, 2, cast_to=int) + if 1 == len(solutions) and solutions[0] == 0: + break + data.append(b) - size = end_ea - begin_ea - data = self.state.memory.load(begin_ea, size=size) self.state.globals['log_messages'].append((level, data)) if 3 == level: @@ -212,9 +218,15 @@ def done_test(state): # Dump out any pending log messages reported by `McTest_Log`. for level, message in state.globals['log_messages']: - if not isinstance(message, str): - message = state.solver.eval(message, cast_to=str) - LEVEL_TO_LOGGER[level]("".join(message)) + data = [] + for b in message: + if not isinstance(b, str): + b = state.solver.eval(b, cast_to=str) + if not ord(b): + break + data.append(b) + + LEVEL_TO_LOGGER[level]("".join(data)) max_length = state.globals['InputEnd'] - state.globals['InputBegin'] if input_length > max_length: @@ -239,7 +251,7 @@ def do_run_test(project, test, apis, run_state): test.ea, base_state=run_state) - messages = [(1, "Running {} from {}:{}".format( + messages = [(1, "Running {} from {}({})".format( test.name, test.file_name, test.line_number))] test_state.globals['InputBegin'] = apis['InputBegin'] @@ -330,6 +342,9 @@ def main(): # Find the test cases that we want to run. tests = find_test_cases(run_state, apis['LastTestInfo']) + L.info("Running {} tests across {} workers".format( + len(tests), args.num_workers)) + pool = multiprocessing.Pool(processes=max(1, args.num_workers)) results = [] diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 4f5ebc6..e9cabff 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -12,7 +12,7 @@ # See the License for the specific language governing permissions and # limitations under the License. -add_executable(OutOfBoundsInt OutOfBoundsInt.c) +add_executable(OutOfBoundsInt OutOfBoundsInt.cpp) target_link_libraries(OutOfBoundsInt mctest) add_executable(ArithmeticProperties ArithmeticProperties.cpp) diff --git a/examples/OutOfBoundsInt.c b/examples/OutOfBoundsInt.cpp similarity index 69% rename from examples/OutOfBoundsInt.c rename to examples/OutOfBoundsInt.cpp index a34cafe..d01f352 100644 --- a/examples/OutOfBoundsInt.c +++ b/examples/OutOfBoundsInt.cpp @@ -14,18 +14,20 @@ * limitations under the License. */ -#include +#include -McTest_EntryPoint(YIsAlwaysPositive) { +TEST(BoundsCheck, YIsAlwaysPositive) { int x = McTest_IntInRange(-10, 10); int y = x * x; - McTest_Assert(y >= 0); + ASSERT_GE(y, 0) + << "Found y=" << y << " was not always positive."; } -McTest_EntryPoint(YIsAlwaysPositive_CanFail) { - int x = McTest_IntInRange(-10, 10); - int y = x * x * x; - McTest_Assert(y >= 0); /* This can fail */ +TEST(BoundsCheck, YIsAlwaysPositive_CanFail) { + int x = McTest_Int(); + int y = x * x; // Can overflow! + ASSERT_GE(y, 0) + << "Found y=" << y << " was not always positive."; } int main(int argc, char *argv[]) { diff --git a/src/include/mctest/McTest.h b/src/include/mctest/McTest.h index dc058a1..8cdc192 100644 --- a/src/include/mctest/McTest.h +++ b/src/include/mctest/McTest.h @@ -269,7 +269,7 @@ static int McTest_Run(void) { for (test = McTest_FirstTest(); test != NULL; test = test->prev) { /* Print the test that we're going to run. */ - num_buff_bytes_used = sprintf(buff, "Running: %s from %s:%u", + num_buff_bytes_used = sprintf(buff, "Running: %s from %s(%u)", test->test_name, test->file_name, test->line_number); McTest_Log(McTest_LogInfo, buff, &(buff[num_buff_bytes_used])); diff --git a/src/lib/McTest.c b/src/lib/McTest.c index ecca27d..a19907c 100644 --- a/src/lib/McTest.c +++ b/src/lib/McTest.c @@ -166,13 +166,15 @@ static const char *McTest_LogLevelStr(enum McTest_LogLevel level) { } } -/* Outputs information to a log, using a specific log level. */ -void McTest_Log(enum McTest_LogLevel level, const char *begin, - const char *end) { - int str_len = (int) (end - begin); - fprintf(stderr, "%s: %.*s\n", McTest_LogLevelStr(level), - str_len, begin); - +enum { + McTest_LogBufSize = 4096 +}; + +char McTest_LogBuf[McTest_LogBufSize + 1] = {}; + + +void _McTest_Log(enum McTest_LogLevel level, const char *message) { + fprintf(stderr, "%s: %s\n", McTest_LogLevelStr(level), message); if (McTest_LogError == level) { McTest_SoftFail(); @@ -181,6 +183,28 @@ void McTest_Log(enum McTest_LogLevel level, const char *begin, } } +/* Outputs information to a log, using a specific log level. */ +void McTest_Log(enum McTest_LogLevel level, const char *begin, + const char *end) { + if (end <= begin) { + return; + } + + size_t size = (size_t) (end - begin); + if (size > McTest_LogBufSize) { + size = McTest_LogBufSize; + } + + /* When we interpose on _McTest_Log, we are looking for the first non-symbolic + * zero byte as our end of string character, so we want to guarantee that we + * have a bunch of those */ + memset(McTest_LogBuf, 0, McTest_LogBufSize); + memcpy(McTest_LogBuf, begin, size); + McTest_LogBuf[McTest_LogBufSize] = '\0'; + + _McTest_Log(level, McTest_LogBuf); +} + /* A McTest-specific symbol that is needed for hooking. */ struct McTest_IndexEntry { const char * const name; @@ -193,7 +217,7 @@ const struct McTest_IndexEntry McTest_API[] = { {"Pass", (void *) McTest_Pass}, {"Fail", (void *) McTest_Fail}, {"SoftFail", (void *) McTest_SoftFail}, - {"Log", (void *) McTest_Log}, + {"Log", (void *) _McTest_Log}, {"Assume", (void *) _McTest_Assume}, {"IsSymbolicUInt", (void *) McTest_IsSymbolicUInt}, {"InputBegin", (void *) &(McTest_Input[0])},