Initial commit.
This commit is contained in:
commit
6249ec6208
69
CMakeLists.txt
Normal file
69
CMakeLists.txt
Normal file
@ -0,0 +1,69 @@
|
||||
# Copyright (c) 2017 Trail of Bits, Inc.
|
||||
#
|
||||
# Licensed under the Apache License, Version 2.0 (the "License");
|
||||
# you may not use this file except in compliance with the License.
|
||||
# You may obtain a copy of the License at
|
||||
#
|
||||
# http://www.apache.org/licenses/LICENSE-2.0
|
||||
#
|
||||
# Unless required by applicable law or agreed to in writing, software
|
||||
# distributed under the License is distributed on an "AS IS" BASIS,
|
||||
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
# See the License for the specific language governing permissions and
|
||||
# limitations under the License.
|
||||
|
||||
project(mctest)
|
||||
cmake_minimum_required(VERSION 2.8)
|
||||
|
||||
enable_language(C)
|
||||
enable_language(CXX)
|
||||
|
||||
find_program(PYTHON "python")
|
||||
|
||||
# Enable the GNU extensions
|
||||
set(CMAKE_CXX_EXTENSIONS ON)
|
||||
|
||||
# Visual Studio already defaults to c++11
|
||||
if (NOT WIN32)
|
||||
set(CMAKE_CXX_STANDARD 11)
|
||||
endif ()
|
||||
|
||||
add_library(${PROJECT_NAME} STATIC
|
||||
src/lib/McTest.c
|
||||
)
|
||||
|
||||
target_include_directories(${PROJECT_NAME}
|
||||
PUBLIC SYSTEM "${CMAKE_SOURCE_DIR}/src/include"
|
||||
)
|
||||
|
||||
# Install the
|
||||
install(
|
||||
DIRECTORY "${CMAKE_SOURCE_DIR}/src/include/mctest"
|
||||
DESTINATION include
|
||||
)
|
||||
|
||||
# Install the library
|
||||
install(
|
||||
TARGETS ${PROJECT_NAME}
|
||||
LIBRARY DESTINATION lib
|
||||
ARCHIVE DESTINATION lib
|
||||
)
|
||||
|
||||
set(SETUP_PY_IN "${CMAKE_SOURCE_DIR}/bin/setup.py.in")
|
||||
set(SETUP_PY "${CMAKE_CURRENT_BINARY_DIR}/setup.py")
|
||||
configure_file(${SETUP_PY_IN} ${SETUP_PY})
|
||||
|
||||
set(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/timestamp")
|
||||
add_custom_command(
|
||||
OUTPUT ${OUTPUT}
|
||||
COMMAND ${PYTHON} ${SETUP_PY} build
|
||||
COMMAND ${CMAKE_COMMAND} -E touch ${OUTPUT}
|
||||
)
|
||||
|
||||
# Install the Manticore harness.
|
||||
add_custom_target(target ALL DEPENDS ${OUTPUT})
|
||||
|
||||
# Install McTest via PIP.
|
||||
install(CODE "execute_process(COMMAND ${PYTHON} ${SETUP_PY} install)")
|
||||
|
||||
add_subdirectory(examples)
|
||||
201
LICENSE
Normal file
201
LICENSE
Normal file
@ -0,0 +1,201 @@
|
||||
Apache License
|
||||
Version 2.0, January 2004
|
||||
http://www.apache.org/licenses/
|
||||
|
||||
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
|
||||
|
||||
1. Definitions.
|
||||
|
||||
"License" shall mean the terms and conditions for use, reproduction,
|
||||
and distribution as defined by Sections 1 through 9 of this document.
|
||||
|
||||
"Licensor" shall mean the copyright owner or entity authorized by
|
||||
the copyright owner that is granting the License.
|
||||
|
||||
"Legal Entity" shall mean the union of the acting entity and all
|
||||
other entities that control, are controlled by, or are under common
|
||||
control with that entity. For the purposes of this definition,
|
||||
"control" means (i) the power, direct or indirect, to cause the
|
||||
direction or management of such entity, whether by contract or
|
||||
otherwise, or (ii) ownership of fifty percent (50%) or more of the
|
||||
outstanding shares, or (iii) beneficial ownership of such entity.
|
||||
|
||||
"You" (or "Your") shall mean an individual or Legal Entity
|
||||
exercising permissions granted by this License.
|
||||
|
||||
"Source" form shall mean the preferred form for making modifications,
|
||||
including but not limited to software source code, documentation
|
||||
source, and configuration files.
|
||||
|
||||
"Object" form shall mean any form resulting from mechanical
|
||||
transformation or translation of a Source form, including but
|
||||
not limited to compiled object code, generated documentation,
|
||||
and conversions to other media types.
|
||||
|
||||
"Work" shall mean the work of authorship, whether in Source or
|
||||
Object form, made available under the License, as indicated by a
|
||||
copyright notice that is included in or attached to the work
|
||||
(an example is provided in the Appendix below).
|
||||
|
||||
"Derivative Works" shall mean any work, whether in Source or Object
|
||||
form, that is based on (or derived from) the Work and for which the
|
||||
editorial revisions, annotations, elaborations, or other modifications
|
||||
represent, as a whole, an original work of authorship. For the purposes
|
||||
of this License, Derivative Works shall not include works that remain
|
||||
separable from, or merely link (or bind by name) to the interfaces of,
|
||||
the Work and Derivative Works thereof.
|
||||
|
||||
"Contribution" shall mean any work of authorship, including
|
||||
the original version of the Work and any modifications or additions
|
||||
to that Work or Derivative Works thereof, that is intentionally
|
||||
submitted to Licensor for inclusion in the Work by the copyright owner
|
||||
or by an individual or Legal Entity authorized to submit on behalf of
|
||||
the copyright owner. For the purposes of this definition, "submitted"
|
||||
means any form of electronic, verbal, or written communication sent
|
||||
to the Licensor or its representatives, including but not limited to
|
||||
communication on electronic mailing lists, source code control systems,
|
||||
and issue tracking systems that are managed by, or on behalf of, the
|
||||
Licensor for the purpose of discussing and improving the Work, but
|
||||
excluding communication that is conspicuously marked or otherwise
|
||||
designated in writing by the copyright owner as "Not a Contribution."
|
||||
|
||||
"Contributor" shall mean Licensor and any individual or Legal Entity
|
||||
on behalf of whom a Contribution has been received by Licensor and
|
||||
subsequently incorporated within the Work.
|
||||
|
||||
2. Grant of Copyright License. Subject to the terms and conditions of
|
||||
this License, each Contributor hereby grants to You a perpetual,
|
||||
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
|
||||
copyright license to reproduce, prepare Derivative Works of,
|
||||
publicly display, publicly perform, sublicense, and distribute the
|
||||
Work and such Derivative Works in Source or Object form.
|
||||
|
||||
3. Grant of Patent License. Subject to the terms and conditions of
|
||||
this License, each Contributor hereby grants to You a perpetual,
|
||||
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
|
||||
(except as stated in this section) patent license to make, have made,
|
||||
use, offer to sell, sell, import, and otherwise transfer the Work,
|
||||
where such license applies only to those patent claims licensable
|
||||
by such Contributor that are necessarily infringed by their
|
||||
Contribution(s) alone or by combination of their Contribution(s)
|
||||
with the Work to which such Contribution(s) was submitted. If You
|
||||
institute patent litigation against any entity (including a
|
||||
cross-claim or counterclaim in a lawsuit) alleging that the Work
|
||||
or a Contribution incorporated within the Work constitutes direct
|
||||
or contributory patent infringement, then any patent licenses
|
||||
granted to You under this License for that Work shall terminate
|
||||
as of the date such litigation is filed.
|
||||
|
||||
4. Redistribution. You may reproduce and distribute copies of the
|
||||
Work or Derivative Works thereof in any medium, with or without
|
||||
modifications, and in Source or Object form, provided that You
|
||||
meet the following conditions:
|
||||
|
||||
(a) You must give any other recipients of the Work or
|
||||
Derivative Works a copy of this License; and
|
||||
|
||||
(b) You must cause any modified files to carry prominent notices
|
||||
stating that You changed the files; and
|
||||
|
||||
(c) You must retain, in the Source form of any Derivative Works
|
||||
that You distribute, all copyright, patent, trademark, and
|
||||
attribution notices from the Source form of the Work,
|
||||
excluding those notices that do not pertain to any part of
|
||||
the Derivative Works; and
|
||||
|
||||
(d) If the Work includes a "NOTICE" text file as part of its
|
||||
distribution, then any Derivative Works that You distribute must
|
||||
include a readable copy of the attribution notices contained
|
||||
within such NOTICE file, excluding those notices that do not
|
||||
pertain to any part of the Derivative Works, in at least one
|
||||
of the following places: within a NOTICE text file distributed
|
||||
as part of the Derivative Works; within the Source form or
|
||||
documentation, if provided along with the Derivative Works; or,
|
||||
within a display generated by the Derivative Works, if and
|
||||
wherever such third-party notices normally appear. The contents
|
||||
of the NOTICE file are for informational purposes only and
|
||||
do not modify the License. You may add Your own attribution
|
||||
notices within Derivative Works that You distribute, alongside
|
||||
or as an addendum to the NOTICE text from the Work, provided
|
||||
that such additional attribution notices cannot be construed
|
||||
as modifying the License.
|
||||
|
||||
You may add Your own copyright statement to Your modifications and
|
||||
may provide additional or different license terms and conditions
|
||||
for use, reproduction, or distribution of Your modifications, or
|
||||
for any such Derivative Works as a whole, provided Your use,
|
||||
reproduction, and distribution of the Work otherwise complies with
|
||||
the conditions stated in this License.
|
||||
|
||||
5. Submission of Contributions. Unless You explicitly state otherwise,
|
||||
any Contribution intentionally submitted for inclusion in the Work
|
||||
by You to the Licensor shall be under the terms and conditions of
|
||||
this License, without any additional terms or conditions.
|
||||
Notwithstanding the above, nothing herein shall supersede or modify
|
||||
the terms of any separate license agreement you may have executed
|
||||
with Licensor regarding such Contributions.
|
||||
|
||||
6. Trademarks. This License does not grant permission to use the trade
|
||||
names, trademarks, service marks, or product names of the Licensor,
|
||||
except as required for reasonable and customary use in describing the
|
||||
origin of the Work and reproducing the content of the NOTICE file.
|
||||
|
||||
7. Disclaimer of Warranty. Unless required by applicable law or
|
||||
agreed to in writing, Licensor provides the Work (and each
|
||||
Contributor provides its Contributions) on an "AS IS" BASIS,
|
||||
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
|
||||
implied, including, without limitation, any warranties or conditions
|
||||
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
|
||||
PARTICULAR PURPOSE. You are solely responsible for determining the
|
||||
appropriateness of using or redistributing the Work and assume any
|
||||
risks associated with Your exercise of permissions under this License.
|
||||
|
||||
8. Limitation of Liability. In no event and under no legal theory,
|
||||
whether in tort (including negligence), contract, or otherwise,
|
||||
unless required by applicable law (such as deliberate and grossly
|
||||
negligent acts) or agreed to in writing, shall any Contributor be
|
||||
liable to You for damages, including any direct, indirect, special,
|
||||
incidental, or consequential damages of any character arising as a
|
||||
result of this License or out of the use or inability to use the
|
||||
Work (including but not limited to damages for loss of goodwill,
|
||||
work stoppage, computer failure or malfunction, or any and all
|
||||
other commercial damages or losses), even if such Contributor
|
||||
has been advised of the possibility of such damages.
|
||||
|
||||
9. Accepting Warranty or Additional Liability. While redistributing
|
||||
the Work or Derivative Works thereof, You may choose to offer,
|
||||
and charge a fee for, acceptance of support, warranty, indemnity,
|
||||
or other liability obligations and/or rights consistent with this
|
||||
License. However, in accepting such obligations, You may act only
|
||||
on Your own behalf and on Your sole responsibility, not on behalf
|
||||
of any other Contributor, and only if You agree to indemnify,
|
||||
defend, and hold each Contributor harmless for any liability
|
||||
incurred by, or claims asserted against, such Contributor by reason
|
||||
of your accepting any such warranty or additional liability.
|
||||
|
||||
END OF TERMS AND CONDITIONS
|
||||
|
||||
APPENDIX: How to apply the Apache License to your work.
|
||||
|
||||
To apply the Apache License to your work, attach the following
|
||||
boilerplate notice, with the fields enclosed by brackets "{}"
|
||||
replaced with your own identifying information. (Don't include
|
||||
the brackets!) The text should be enclosed in the appropriate
|
||||
comment syntax for the file format. We also recommend that a
|
||||
file or class name and description of purpose be included on the
|
||||
same "printed page" as the copyright notice for easier
|
||||
identification within third-party archives.
|
||||
|
||||
Copyright 2017 Trail of Bits, Inc.
|
||||
|
||||
Licensed under the Apache License, Version 2.0 (the "License");
|
||||
you may not use this file except in compliance with the License.
|
||||
You may obtain a copy of the License at
|
||||
|
||||
http://www.apache.org/licenses/LICENSE-2.0
|
||||
|
||||
Unless required by applicable law or agreed to in writing, software
|
||||
distributed under the License is distributed on an "AS IS" BASIS,
|
||||
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
See the License for the specific language governing permissions and
|
||||
limitations under the License.
|
||||
0
bin/mctest/__init__.py
Normal file
0
bin/mctest/__init__.py
Normal file
166
bin/mctest/__main__.py
Normal file
166
bin/mctest/__main__.py
Normal file
@ -0,0 +1,166 @@
|
||||
#!/usr/bin/env python
|
||||
# Copyright (c) 2017 Trail of Bits, Inc.
|
||||
#
|
||||
# Licensed under the Apache License, Version 2.0 (the "License");
|
||||
# you may not use this file except in compliance with the License.
|
||||
# You may obtain a copy of the License at
|
||||
#
|
||||
# http://www.apache.org/licenses/LICENSE-2.0
|
||||
#
|
||||
# Unless required by applicable law or agreed to in writing, software
|
||||
# distributed under the License is distributed on an "AS IS" BASIS,
|
||||
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
# See the License for the specific language governing permissions and
|
||||
# limitations under the License.
|
||||
|
||||
import angr
|
||||
import sys
|
||||
|
||||
def read_c_string(state, ea):
|
||||
"""Read a concrete NUL-terminated string from `ea`."""
|
||||
assert isinstance(ea, (int, long))
|
||||
chars = []
|
||||
i = 0
|
||||
while True:
|
||||
char = state.mem[ea + i].char.resolved
|
||||
char = state.solver.eval(char, cast_to=str)
|
||||
if not ord(char[0]):
|
||||
break
|
||||
chars.append(char)
|
||||
i += 1
|
||||
return "".join(chars)
|
||||
|
||||
|
||||
def read_uint64_t(state, ea):
|
||||
"""Read a uint64_t value from memory."""
|
||||
return state.solver.eval(state.mem[ea].uint64_t.resolved,
|
||||
cast_to=int)
|
||||
|
||||
|
||||
def find_test_cases(project, state):
|
||||
"""Find the test case descriptors."""
|
||||
obj = project.loader.main_object
|
||||
tests = []
|
||||
for sec in obj.sections:
|
||||
if sec.name != ".mctest_entrypoints":
|
||||
continue
|
||||
for ea in xrange(sec.vaddr, sec.vaddr + sec.memsize, 32):
|
||||
test_func_ea = read_uint64_t(state, ea + 0)
|
||||
test_name_ea = read_uint64_t(state, ea + 8)
|
||||
file_name_ea = read_uint64_t(state, ea + 16)
|
||||
file_line_num = read_uint64_t(state, ea + 24)
|
||||
|
||||
test_name = read_c_string(state, test_name_ea)
|
||||
file_name = read_c_string(state, file_name_ea)
|
||||
|
||||
tests.append((test_func_ea, test_name, file_name, file_line_num))
|
||||
return tests
|
||||
|
||||
|
||||
def hook_symbolic_int_func(project, state, name, num_bits):
|
||||
"""Hook a McTest function and make it return a symbolic integer."""
|
||||
class Function(angr.SimProcedure):
|
||||
def run(self):
|
||||
return self.state.solver.BVS("", num_bits)
|
||||
|
||||
func_name = "McTest_{}".format(name)
|
||||
ea = project.kb.labels.lookup(func_name)
|
||||
project.hook(ea, Function(project=project))
|
||||
|
||||
|
||||
def hook_predicate_int_func(project, state, name, num_bits):
|
||||
"""Hook a McTest function that checks whether or not its integer argument
|
||||
is symbolic."""
|
||||
class Function(angr.SimProcedure):
|
||||
def run(self, arg):
|
||||
return int(self.state.se.symbolic(arg))
|
||||
|
||||
func_name = "McTest_IsSymbolic{}".format(name)
|
||||
ea = project.kb.labels.lookup(func_name)
|
||||
project.hook(ea, Function(project=project))
|
||||
|
||||
|
||||
class Assume(angr.SimProcedure):
|
||||
"""Implements McTest_Assume, which injects a constraint."""
|
||||
def run(self, arg):
|
||||
if self.state.se.symbolic(arg):
|
||||
constraint = arg != 0
|
||||
eval_res = self.state.se.eval(constraint)
|
||||
if eval_res:
|
||||
self.state.add_constraints(constraint)
|
||||
ret = eval_res
|
||||
else:
|
||||
ret = self.state.se.eval(arg) != 0
|
||||
return int(ret)
|
||||
|
||||
|
||||
def main():
|
||||
"""Run McTest."""
|
||||
if 2 > len(sys.argv):
|
||||
return 1
|
||||
|
||||
project = angr.Project(
|
||||
sys.argv[1],
|
||||
use_sim_procedures=True,
|
||||
translation_cache=True,
|
||||
support_selfmodifying_code=False)
|
||||
|
||||
entry_state = project.factory.entry_state()
|
||||
addr_size_bits = entry_state.arch.bits
|
||||
|
||||
# Find the test cases that we want to run.
|
||||
tests = find_test_cases(project, entry_state)
|
||||
|
||||
# Concretely execute up until `main`.
|
||||
concrete_manager = angr.SimulationManager(
|
||||
project=project,
|
||||
active_states=[entry_state])
|
||||
ea_of_main = project.kb.labels.lookup('main')
|
||||
concrete_manager.explore(find=ea_of_main)
|
||||
main_state = concrete_manager.found[0]
|
||||
|
||||
#concrete_manager.move(from_stash='found', to_stash='deadended')
|
||||
|
||||
# Hook functions that should now return symbolic values.
|
||||
hook_symbolic_int_func(project, main_state, 'Bool', 1)
|
||||
hook_symbolic_int_func(project, main_state, 'Size', addr_size_bits)
|
||||
hook_symbolic_int_func(project, main_state, 'UInt64', 64)
|
||||
hook_symbolic_int_func(project, main_state, 'UInt', 32)
|
||||
|
||||
# Hook predicate functions that should return 1 or 0 depending on whether
|
||||
# or not their argument is symbolic.
|
||||
hook_predicate_int_func(project, main_state, 'UInt', 32)
|
||||
|
||||
# Hook the assume function.
|
||||
project.hook(project.kb.labels.lookup('McTest_Assume'),
|
||||
Assume(project=project))
|
||||
|
||||
ea_of_done = project.kb.labels.lookup('McTest_DoneTestCase')
|
||||
|
||||
# For each test, create a simulation manager whose initial state calls into
|
||||
# the test case function, and returns to `McTest_DoneTestCase`.
|
||||
test_managers = []
|
||||
for entry_ea, test_name, file_name, line_num in tests:
|
||||
test_state = project.factory.call_state(
|
||||
entry_ea,
|
||||
base_state=main_state,
|
||||
ret_addr=ea_of_done)
|
||||
|
||||
# NOTE(pag): Enabling Veritesting seems to miss some cases where the
|
||||
# tests fail.
|
||||
test_manager = angr.SimulationManager(
|
||||
project=project,
|
||||
active_states=[test_state])
|
||||
|
||||
test_manager.run()
|
||||
|
||||
for state in test_manager.deadended:
|
||||
last_event = state.history.events[-1]
|
||||
if 'terminate' == last_event.type:
|
||||
code = last_event.objects['exit_code']._model_concrete.value
|
||||
print "{} in {}:{} terminated with {}".format(test_name, file_name, line_num, code)
|
||||
|
||||
return 0
|
||||
|
||||
if "__main__" == __name__:
|
||||
exit(main())
|
||||
38
bin/setup.py.in
Normal file
38
bin/setup.py.in
Normal file
@ -0,0 +1,38 @@
|
||||
#!/usr/bin/env python
|
||||
# Copyright (c) 2017 Trail of Bits, Inc.
|
||||
#
|
||||
# Licensed under the Apache License, Version 2.0 (the "License");
|
||||
# you may not use this file except in compliance with the License.
|
||||
# You may obtain a copy of the License at
|
||||
#
|
||||
# http://www.apache.org/licenses/LICENSE-2.0
|
||||
#
|
||||
# Unless required by applicable law or agreed to in writing, software
|
||||
# distributed under the License is distributed on an "AS IS" BASIS,
|
||||
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
# See the License for the specific language governing permissions and
|
||||
# limitations under the License.
|
||||
|
||||
import distutils.core
|
||||
import os
|
||||
import setuptools
|
||||
|
||||
MCTEST_DIR = os.path.dirname(os.path.realpath(__file__))
|
||||
|
||||
setuptools.setup(
|
||||
name="mctest",
|
||||
version="0.1",
|
||||
package_dir={"": "${CMAKE_SOURCE_DIR}/bin"},
|
||||
packages=['mctest'],
|
||||
description="McTest augments C/C++ Test-Driven Development with Symbolic Execution",
|
||||
url="https://github.com/trailofbits/mctest",
|
||||
author="Peter Goodman",
|
||||
author_email="peter@trailofbits.com",
|
||||
license="Apache-2.0",
|
||||
keywords="tdd testing symbolic execution",
|
||||
install_requires=['angr'],
|
||||
entry_points={
|
||||
'console_scripts': [
|
||||
'mctest = mctest.__main__:main'
|
||||
]
|
||||
})
|
||||
16
examples/CMakeLists.txt
Normal file
16
examples/CMakeLists.txt
Normal file
@ -0,0 +1,16 @@
|
||||
# Copyright (c) 2017 Trail of Bits, Inc.
|
||||
#
|
||||
# Licensed under the Apache License, Version 2.0 (the "License");
|
||||
# you may not use this file except in compliance with the License.
|
||||
# You may obtain a copy of the License at
|
||||
#
|
||||
# http://www.apache.org/licenses/LICENSE-2.0
|
||||
#
|
||||
# Unless required by applicable law or agreed to in writing, software
|
||||
# distributed under the License is distributed on an "AS IS" BASIS,
|
||||
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
# See the License for the specific language governing permissions and
|
||||
# limitations under the License.
|
||||
|
||||
add_executable(OutOfBoundsInt OutOfBoundsInt.c)
|
||||
target_link_libraries(OutOfBoundsInt mctest)
|
||||
29
examples/OutOfBoundsInt.c
Normal file
29
examples/OutOfBoundsInt.c
Normal file
@ -0,0 +1,29 @@
|
||||
/*
|
||||
* Copyright (c) 2017 Trail of Bits, Inc.
|
||||
*
|
||||
* Licensed under the Apache License, Version 2.0 (the "License");
|
||||
* you may not use this file except in compliance with the License.
|
||||
* You may obtain a copy of the License at
|
||||
*
|
||||
* http://www.apache.org/licenses/LICENSE-2.0
|
||||
*
|
||||
* Unless required by applicable law or agreed to in writing, software
|
||||
* distributed under the License is distributed on an "AS IS" BASIS,
|
||||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
* See the License for the specific language governing permissions and
|
||||
* limitations under the License.
|
||||
*/
|
||||
|
||||
#include <mctest/McTest.h>
|
||||
|
||||
McTest_EntryPoint(YIsAlwaysPositive) {
|
||||
int x = McTest_IntInRange(-10, 10);
|
||||
int y = x * x;
|
||||
McTest_Assert(y >= 0);
|
||||
}
|
||||
|
||||
McTest_EntryPoint(YIsAlwaysPositive_WillFail) {
|
||||
int x = McTest_IntInRange(-10, 10);
|
||||
int y = x * x * x;
|
||||
McTest_Assert(y >= 0); /* This will fail */
|
||||
}
|
||||
241
src/include/mctest/McTest.h
Normal file
241
src/include/mctest/McTest.h
Normal file
@ -0,0 +1,241 @@
|
||||
/*
|
||||
* Copyright (c) 2017 Trail of Bits, Inc.
|
||||
*
|
||||
* Licensed under the Apache License, Version 2.0 (the "License");
|
||||
* you may not use this file except in compliance with the License.
|
||||
* You may obtain a copy of the License at
|
||||
*
|
||||
* http://www.apache.org/licenses/LICENSE-2.0
|
||||
*
|
||||
* Unless required by applicable law or agreed to in writing, software
|
||||
* distributed under the License is distributed on an "AS IS" BASIS,
|
||||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
* See the License for the specific language governing permissions and
|
||||
* limitations under the License.
|
||||
*/
|
||||
|
||||
#ifndef INCLUDE_MCTEST_MCTEST_H_
|
||||
#define INCLUDE_MCTEST_MCTEST_H_
|
||||
|
||||
#include <stddef.h>
|
||||
#include <stdint.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif /* __cplusplus */
|
||||
|
||||
/* Symbolize the data in the range `[begin, end)`. */
|
||||
extern void McTest_SymbolizeData(void *begin, void *end);
|
||||
|
||||
inline static void *McTest_Malloc(size_t num_bytes) {
|
||||
void *data = malloc(num_bytes);
|
||||
uintptr_t data_end = ((uintptr_t) data) + num_bytes;
|
||||
McTest_SymbolizeData(data, (void *) data_end);
|
||||
return data;
|
||||
}
|
||||
|
||||
#define MCTEST_MAKE_SYMBOLIC_ARRAY(Tname, tname) \
|
||||
inline static tname *McTest_Symbolic ## Tname ## Array(size_t num_elms) { \
|
||||
tname *arr = (tname *) malloc(sizeof(tname) * num_elms); \
|
||||
McTest_SymbolizeData(arr, &(arr[num_elms])); \
|
||||
return arr; \
|
||||
}
|
||||
|
||||
MCTEST_MAKE_SYMBOLIC_ARRAY(Int64, int64_t)
|
||||
MCTEST_MAKE_SYMBOLIC_ARRAY(UInt64, uint64_t)
|
||||
MCTEST_MAKE_SYMBOLIC_ARRAY(Int, int)
|
||||
MCTEST_MAKE_SYMBOLIC_ARRAY(UInt, uint32_t)
|
||||
MCTEST_MAKE_SYMBOLIC_ARRAY(Short, int16_t)
|
||||
MCTEST_MAKE_SYMBOLIC_ARRAY(UShort, uint16_t)
|
||||
MCTEST_MAKE_SYMBOLIC_ARRAY(Char, char)
|
||||
MCTEST_MAKE_SYMBOLIC_ARRAY(UChar, unsigned char)
|
||||
|
||||
#undef MCTEST_MAKE_SYMBOLIC_ARRAY
|
||||
|
||||
/* Return a symbolic C string. */
|
||||
inline static char *McTest_CStr(size_t len) {
|
||||
char *str = (char *) malloc(sizeof(char) * len);
|
||||
if (len) {
|
||||
McTest_SymbolizeData(str, &(str[len - 1]));
|
||||
str[len - 1] = '\0';
|
||||
}
|
||||
return str;
|
||||
}
|
||||
|
||||
/* Creates an assumption about a symbolic value. Returns `1` if the assumption
|
||||
* can hold and was asserted. */
|
||||
extern int McTest_Assume(int expr);
|
||||
|
||||
/* Asserts that `expr` must hold. */
|
||||
inline static void McTest_Assert(int expr) {
|
||||
if (McTest_Assume(!expr)) {
|
||||
abort();
|
||||
}
|
||||
}
|
||||
|
||||
/* Return a symbolic value of a given type. */
|
||||
extern int McTest_Bool(void);
|
||||
extern size_t McTest_Size(void);
|
||||
extern uint64_t McTest_UInt64(void);
|
||||
extern uint32_t McTest_UInt(void);
|
||||
|
||||
inline static int64_t McTest_Int64(void) {
|
||||
return (int64_t) McTest_UInt64();
|
||||
}
|
||||
|
||||
inline static int32_t McTest_Int(void) {
|
||||
return (int32_t) McTest_UInt();
|
||||
}
|
||||
|
||||
inline static uint16_t McTest_UShort(void) {
|
||||
return (uint16_t) McTest_UInt();
|
||||
}
|
||||
|
||||
inline static int16_t McTest_Short(void) {
|
||||
return (int16_t) McTest_UInt();
|
||||
}
|
||||
|
||||
inline static unsigned char McTest_UChar(void) {
|
||||
return (unsigned char) McTest_UInt();
|
||||
}
|
||||
|
||||
inline static char McTest_Char(void) {
|
||||
return (char) McTest_UInt();
|
||||
}
|
||||
|
||||
/* Return a symbolic value in a the range `[low_inc, high_inc]`. */
|
||||
#define MCTEST_MAKE_SYMBOLIC_RANGE(Tname, tname) \
|
||||
inline static tname McTest_ ## Tname ## InRange( \
|
||||
tname low, tname high) { \
|
||||
tname x = McTest_ ## Tname(); \
|
||||
(void) McTest_Assume(low <= x && x <= high); \
|
||||
return x; \
|
||||
}
|
||||
|
||||
MCTEST_MAKE_SYMBOLIC_RANGE(Int64, int64_t)
|
||||
MCTEST_MAKE_SYMBOLIC_RANGE(UInt64, uint64_t)
|
||||
MCTEST_MAKE_SYMBOLIC_RANGE(Int, int)
|
||||
MCTEST_MAKE_SYMBOLIC_RANGE(UInt, uint32_t)
|
||||
MCTEST_MAKE_SYMBOLIC_RANGE(Short, int16_t)
|
||||
MCTEST_MAKE_SYMBOLIC_RANGE(UShort, uint16_t)
|
||||
MCTEST_MAKE_SYMBOLIC_RANGE(Char, char)
|
||||
MCTEST_MAKE_SYMBOLIC_RANGE(UChar, unsigned char)
|
||||
|
||||
#undef MCTEST_MAKE_SYMBOLIC_RANGE
|
||||
|
||||
|
||||
/* Return a symbolic value of a given type. */
|
||||
extern int McTest_Bool(void);
|
||||
extern size_t McTest_Size(void);
|
||||
extern uint64_t McTest_UInt64(void);
|
||||
extern int64_t McTest_Int64(void);
|
||||
extern uint32_t McTest_UInt(void);
|
||||
extern int32_t McTest_Int(void);
|
||||
extern uint16_t McTest_UShort(void);
|
||||
extern int16_t McTest_Short(void);
|
||||
extern unsigned char McTest_UChar(void);
|
||||
extern char McTest_Char(void);
|
||||
|
||||
/* Predicates to check whether or not a particular value is symbolic */
|
||||
extern int McTest_IsSymbolicUInt(uint32_t x);
|
||||
|
||||
inline static int McTest_IsSymbolicInt(int x) {
|
||||
return McTest_IsSymbolicUInt((uint32_t) x);
|
||||
}
|
||||
|
||||
inline static int McTest_IsSymbolicUShort(uint16_t x) {
|
||||
return McTest_IsSymbolicUInt((uint32_t) x);
|
||||
}
|
||||
|
||||
inline static int McTest_IsSymbolicShort(int16_t x) {
|
||||
return McTest_IsSymbolicUInt((uint32_t) (uint16_t) x);
|
||||
}
|
||||
|
||||
inline static int McTest_IsSymbolicUChar(unsigned char x) {
|
||||
return McTest_IsSymbolicUInt((uint32_t) x);
|
||||
}
|
||||
|
||||
inline static int McTest_IsSymbolicChar(char x) {
|
||||
return McTest_IsSymbolicUInt((uint32_t) (unsigned char) x);
|
||||
}
|
||||
|
||||
inline static int McTest_IsSymbolicUInt64(uint64_t x) {
|
||||
return McTest_IsSymbolicUInt((uint32_t) x) ||
|
||||
McTest_IsSymbolicUInt((uint32_t) (x >> 32U));
|
||||
}
|
||||
|
||||
inline static int McTest_IsSymbolicInt64(int64_t x) {
|
||||
return McTest_IsSymbolicUInt64((uint64_t) x);
|
||||
}
|
||||
|
||||
inline static int McTest_IsSymbolicBool(int x) {
|
||||
return McTest_IsSymbolicInt(x);
|
||||
}
|
||||
|
||||
#pragma clang diagnostic push
|
||||
#pragma clang diagnostic ignored "-Wpointer-to-int-cast"
|
||||
|
||||
#pragma GCC diagnostic push
|
||||
#pragma GCC diagnostic ignored "-Wpointer-to-int-cast"
|
||||
|
||||
inline static int McTest_IsSymbolicPtr(void *x) {
|
||||
if (sizeof(void *) == 8) {
|
||||
return McTest_IsSymbolicUInt64((uint64_t) x);
|
||||
} else {
|
||||
return McTest_IsSymbolicUInt((uint32_t) x);
|
||||
}
|
||||
}
|
||||
|
||||
#pragma GCC diagnostic pop
|
||||
#pragma clang diagnostic pop
|
||||
|
||||
inline static int McTest_IsSymbolicFloat(float x) {
|
||||
return McTest_IsSymbolicUInt(*((uint32_t *) &x));
|
||||
}
|
||||
|
||||
inline static int McTest_IsSymbolicDouble(double x) {
|
||||
return McTest_IsSymbolicUInt64(*((uint64_t *) &x));
|
||||
}
|
||||
|
||||
#define _MCTEST_TO_STR(a) __MCTEST_TO_STR(a)
|
||||
#define __MCTEST_TO_STR(a) #a
|
||||
|
||||
#ifdef __cplusplus
|
||||
# define MCTEST_EXTERN_C extern "C"
|
||||
#else
|
||||
# define MCTEST_EXTERN_C
|
||||
#endif
|
||||
|
||||
#define McTest_EntryPoint(test_name) \
|
||||
_McTest_EntryPoint(test_name, __FILE__, __LINE__)
|
||||
|
||||
#define _McTest_EntryPoint(test_name, file, line) \
|
||||
static void McTest_Run_ ## test_name (void); \
|
||||
__attribute__((noinline, used)) \
|
||||
MCTEST_EXTERN_C void McTest_Register_ ## test_name (void) { \
|
||||
__asm__ __volatile__ ( \
|
||||
".pushsection .mctest_strtab,\"a\" \n" \
|
||||
"1: \n" \
|
||||
".asciz \"" _MCTEST_TO_STR(test_name) "\" \n" \
|
||||
"2: \n" \
|
||||
".asciz \"" file "\" \n" \
|
||||
".popsection \n" \
|
||||
".pushsection .mctest_entrypoints,\"a\" \n" \
|
||||
".balign 16 \n" \
|
||||
".quad %p0 \n" \
|
||||
".quad 1b \n" \
|
||||
".quad 2b \n" \
|
||||
".quad " _MCTEST_TO_STR(line) " \n" \
|
||||
".popsection \n" \
|
||||
: \
|
||||
: "i"(McTest_Run_ ## test_name) \
|
||||
); \
|
||||
} \
|
||||
void McTest_Run_ ## test_name(void)
|
||||
|
||||
|
||||
#ifdef __cplusplus
|
||||
} /* extern C */
|
||||
#endif /* __cplusplus */
|
||||
#endif /* INCLUDE_MCTEST_MCTEST_H_ */
|
||||
149
src/include/mctest/McTest.hpp
Normal file
149
src/include/mctest/McTest.hpp
Normal file
@ -0,0 +1,149 @@
|
||||
/*
|
||||
* Copyright (c) 2017 Trail of Bits, Inc.
|
||||
*
|
||||
* Licensed under the Apache License, Version 2.0 (the "License");
|
||||
* you may not use this file except in compliance with the License.
|
||||
* You may obtain a copy of the License at
|
||||
*
|
||||
* http://www.apache.org/licenses/LICENSE-2.0
|
||||
*
|
||||
* Unless required by applicable law or agreed to in writing, software
|
||||
* distributed under the License is distributed on an "AS IS" BASIS,
|
||||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
* See the License for the specific language governing permissions and
|
||||
* limitations under the License.
|
||||
*/
|
||||
|
||||
#ifndef INCLUDE_MCTEST_MCTEST_HPP_
|
||||
#define INCLUDE_MCTEST_MCTEST_HPP_
|
||||
|
||||
#include <mctest/McTest.h>
|
||||
|
||||
#include <string>
|
||||
#include <utility>
|
||||
#include <vector>
|
||||
|
||||
namespace mctest {
|
||||
|
||||
inline static void *Malloc(size_t num_bytes) {
|
||||
return McTest_Malloc(num_bytes);
|
||||
}
|
||||
|
||||
inline static void SymbolizeData(void *begin, void *end) {
|
||||
McTest_SymbolizeData(begin, end);
|
||||
}
|
||||
|
||||
inline static bool Bool(void) {
|
||||
return static_cast<bool>(McTest_Bool());
|
||||
}
|
||||
|
||||
inline static size_t Size(void) {
|
||||
return McTest_Size();
|
||||
}
|
||||
|
||||
inline static uint64_t UInt64(void) {
|
||||
return McTest_UInt64();
|
||||
}
|
||||
|
||||
inline static int64_t Int64(void) {
|
||||
return McTest_Int64();
|
||||
}
|
||||
|
||||
inline static uint32_t UInt(void) {
|
||||
return McTest_UInt();
|
||||
}
|
||||
|
||||
inline static int32_t Int(void) {
|
||||
return McTest_Int();
|
||||
}
|
||||
|
||||
inline static uint16_t UShort(void) {
|
||||
return McTest_UShort();
|
||||
}
|
||||
|
||||
inline static int16_t Short(void) {
|
||||
return McTest_Short();
|
||||
}
|
||||
|
||||
inline static unsigned char UChar(void) {
|
||||
return McTest_UChar();
|
||||
}
|
||||
|
||||
inline static char Char(void) {
|
||||
return McTest_Char();
|
||||
}
|
||||
|
||||
inline static int IsSymbolic(uint64_t x) {
|
||||
return McTest_IsSymbolicUInt64(x);
|
||||
}
|
||||
|
||||
inline static int IsSymbolic(int64_t x) {
|
||||
return McTest_IsSymbolicInt64(x);
|
||||
}
|
||||
|
||||
inline static int IsSymbolic(uint32_t x) {
|
||||
return McTest_IsSymbolicUInt(x);
|
||||
}
|
||||
|
||||
inline static int IsSymbolic(int32_t x) {
|
||||
return McTest_IsSymbolicInt(x);
|
||||
}
|
||||
|
||||
inline static int IsSymbolic(uint16_t x) {
|
||||
return McTest_IsSymbolicUShort(x);
|
||||
}
|
||||
|
||||
inline static int IsSymbolic(int16_t x) {
|
||||
return McTest_IsSymbolicShort(x);
|
||||
}
|
||||
|
||||
inline static int IsSymbolic(unsigned char x) {
|
||||
return McTest_IsSymbolicUChar(x);
|
||||
}
|
||||
|
||||
inline static int IsSymbolic(char x) {
|
||||
return McTest_IsSymbolicChar(x);
|
||||
}
|
||||
|
||||
inline static int IsSymbolic(float x) {
|
||||
return McTest_IsSymbolicFloat(x);
|
||||
}
|
||||
|
||||
inline static int IsSymbolic(double x) {
|
||||
return McTest_IsSymbolicDouble(x);
|
||||
}
|
||||
|
||||
inline static int IsSymbolic(void *x) {
|
||||
return McTest_IsSymbolicPtr(x);
|
||||
}
|
||||
|
||||
#if 199711L < __cplusplus
|
||||
|
||||
/* Returns a symbolic container (where it makes sense). Container entries
|
||||
* do not necessarily need to be contiguous. */
|
||||
template <typename ContainerT, typename... Args>
|
||||
inline static ContainerT Symbolic(Args&& ...args) {
|
||||
ContainerT cont(std::forward<Args...>(args)...);
|
||||
if (!cont.empty()) {
|
||||
for (auto &entry : cont) {
|
||||
auto entry_ptr = &entry;
|
||||
McTest_SymbolizeData(entry_ptr, &(entry_ptr[1]));
|
||||
}
|
||||
}
|
||||
return cont;
|
||||
}
|
||||
|
||||
#endif // 199711L < __cplusplus
|
||||
|
||||
// Returns a symbolic std::string of length `len`.
|
||||
inline static std::string Str(size_t len) {
|
||||
std::string str(len);
|
||||
if (len) {
|
||||
McTest_SymbolizeData(&(str.begin()), &(str.end()));
|
||||
}
|
||||
return str;
|
||||
}
|
||||
|
||||
} // namespace mctest
|
||||
|
||||
#endif // INCLUDE_MCTEST_MCTEST_HPP_
|
||||
76
src/lib/McTest.c
Normal file
76
src/lib/McTest.c
Normal file
@ -0,0 +1,76 @@
|
||||
/*
|
||||
* Copyright (c) 2017 Trail of Bits, Inc.
|
||||
*
|
||||
* Licensed under the Apache License, Version 2.0 (the "License");
|
||||
* you may not use this file except in compliance with the License.
|
||||
* You may obtain a copy of the License at
|
||||
*
|
||||
* http://www.apache.org/licenses/LICENSE-2.0
|
||||
*
|
||||
* Unless required by applicable law or agreed to in writing, software
|
||||
* distributed under the License is distributed on an "AS IS" BASIS,
|
||||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
* See the License for the specific language governing permissions and
|
||||
* limitations under the License.
|
||||
*/
|
||||
|
||||
#include <mctest/McTest.h>
|
||||
|
||||
#include <assert.h>
|
||||
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif /* __cplusplus */
|
||||
|
||||
static uint32_t gPlaybookIndex = 0;
|
||||
static uint32_t gPlaybook[8192] = {};
|
||||
|
||||
void McTest_SymbolizeData(void *begin, void *end) {
|
||||
(void) begin;
|
||||
(void) end;
|
||||
}
|
||||
|
||||
/* Return a symbolic value of a given type. */
|
||||
int McTest_Bool(void) {
|
||||
return 0;
|
||||
}
|
||||
|
||||
size_t McTest_Size(void) {
|
||||
return 0;
|
||||
}
|
||||
|
||||
uint64_t McTest_UInt64(void) {
|
||||
return 0;
|
||||
}
|
||||
|
||||
uint32_t McTest_UInt(void) {
|
||||
return 0;
|
||||
}
|
||||
|
||||
int McTest_Assume(int expr) {
|
||||
assert(expr);
|
||||
return 1;
|
||||
}
|
||||
|
||||
int McTest_IsSymbolicUInt(uint32_t x) {
|
||||
(void) x;
|
||||
return 0;
|
||||
}
|
||||
|
||||
void McTest_DoneTestCase(void) {
|
||||
exit(EXIT_SUCCESS);
|
||||
}
|
||||
|
||||
/* McTest implements the `main` function so that test code can focus on tests */
|
||||
int main(void) {
|
||||
#if defined(__x86_64__) || defined(__i386__) || defined(_M_X86)
|
||||
asm("ud2; .asciz \"I'm McTest'in it\";");
|
||||
#else
|
||||
# error "Unsupported platform (for now)."
|
||||
#endif
|
||||
return EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
#ifdef __cplusplus
|
||||
} /* extern C */
|
||||
#endif /* __cplusplus */
|
||||
Loading…
x
Reference in New Issue
Block a user