diff --git a/examples/script/symbolic_file.py b/examples/script/symbolic_file.py new file mode 100755 index 000000000..73d5a2e12 --- /dev/null +++ b/examples/script/symbolic_file.py @@ -0,0 +1,77 @@ +#!/usr/bin/env python + +""" +Example to show usage of introducing a file with symbolic contents + +This script should be the equivalent of: + $ echo "+++++++++++++" > symbolic_file.txt + $ manticore -v --file symbolic_file.txt ../linux/fileio symbolic_file.txt +""" +import copy +import glob +import os +import pathlib +import sys +import tempfile + +from manticore.__main__ import main + + +def test_symbolic_file(tmp_path): + # Run this file with Manticore + filepath = pathlib.Path(__file__).resolve().parent.parent / pathlib.Path("linux/fileio") + assert filepath.exists(), f"Please run the Makefile in {filepath.parent} to build {filepath}" + + # Temporary workspace for Manticore + workspace_dir = tmp_path / "mcore_workspace" + workspace_dir.mkdir(parents=True, exist_ok=True) + assert ( + len(os.listdir(workspace_dir)) == 0 + ), f"Manticore workspace {workspace_dir} should be empty before running" + + # Manticore will search for and read this partially symbolic file + sym_file_name = "symbolic_file.txt" + sym_file = tmp_path / sym_file_name + sym_file.write_text("+++++++++++++") + + # Program arguments that would be passed to Manticore via CLI + manticore_args = [ + # Show some progress + "-v", + # Register our symbolic file with Manticore + "--file", + str(sym_file), + # Setup workspace, for this test, or omit to use current directory + "--workspace", + str(workspace_dir), + # Manticore will execute our file here with arguments + str(filepath), + str(sym_file), + ] + + # Bad hack to workaround passing the above arguments like we do on command + # line and have them parsed with argparse + backup_argv = copy.deepcopy(sys.argv[1:]) + del sys.argv[1:] + sys.argv.extend(manticore_args) + + # Call Manticore's main with our new argv list for argparse + main() + + del sys.argv[1:] + sys.argv.extend(backup_argv) + + # Manticore will write out the concretized contents of our symbolic file for + # each path in the program + all_concretized_sym_files = glob.glob(str(workspace_dir / f"*{sym_file_name}")) + assert ( + len(all_concretized_sym_files) > 1 + ), "Should have found more than 1 path through the program" + assert any( + map(lambda f: b"open sesame" in pathlib.Path(f).read_bytes(), all_concretized_sym_files) + ), "Could not find 'open sesame' in our concretized symbolic file" + + +if __name__ == "__main__": + with tempfile.TemporaryDirectory() as workspace: + test_symbolic_file(pathlib.Path(workspace)) diff --git a/manticore/platforms/linux.py b/manticore/platforms/linux.py index 98cb55a66..6d4f41670 100644 --- a/manticore/platforms/linux.py +++ b/manticore/platforms/linux.py @@ -474,6 +474,13 @@ def __init__( """ super().__init__(path, flags) + # Convert to numeric value because we read the file as bytes + wildcard_buf: bytes = wildcard.encode() + assert ( + len(wildcard_buf) == 1 + ), f"SymbolicFile wildcard needs to be a single byte, not {wildcard_buf!r}" + wildcard_val = wildcard_buf[0] + # read the concrete data using the parent the read() form the File class data = self.file.read() @@ -487,7 +494,7 @@ def __init__( symbols_cnt = 0 for i in range(size): - if data[i] != wildcard: + if data[i] != wildcard_val: self.array[i] = data[i] else: symbols_cnt += 1 diff --git a/scripts/run_tests.sh b/scripts/run_tests.sh index 7ebeb21b0..745ebd5f2 100755 --- a/scripts/run_tests.sh +++ b/scripts/run_tests.sh @@ -48,6 +48,12 @@ launch_examples() { return 1 fi + echo "Running fileio symbolic file test..." + coverage run --append ./symbolic_file.py + if [ $? -ne 0 ]; then + return 1 + fi + return 0 } diff --git a/tests/native/test_integration_native.py b/tests/native/test_integration_native.py index 2821c559d..53e992064 100644 --- a/tests/native/test_integration_native.py +++ b/tests/native/test_integration_native.py @@ -287,12 +287,6 @@ def test_fclose_linux_amd64(self) -> None: """ self._test_no_crash("fclose_linux_amd64", "+++++++") - def test_fileio_linux_amd64(self) -> None: - """ - Tests that the `fileio` example for amd64 linux doesn't crash. - """ - self._test_no_crash("fileio_linux_amd64", "+") - def test_ioctl_bogus(self) -> None: """ Tests that the `ioctl_bogus_linux_amd64` example for amd64 linux doesn't crash. diff --git a/tests/native/test_linux.py b/tests/native/test_linux.py index 9f9bd3df9..028cac39c 100644 --- a/tests/native/test_linux.py +++ b/tests/native/test_linux.py @@ -1,4 +1,5 @@ import errno +import logging import unittest from binascii import hexlify @@ -10,11 +11,11 @@ from manticore.native.cpu.abstractcpu import ConcretizeRegister from manticore.core.smtlib.solver import Z3Solver -from manticore.core.smtlib import BitVecVariable, issymbolic +from manticore.core.smtlib import BitVecVariable, issymbolic, ConstraintSet from manticore.native import Manticore from manticore.platforms import linux, linux_syscalls from manticore.utils.helpers import pickle_dumps -from manticore.platforms.linux import EnvironmentError +from manticore.platforms.linux import EnvironmentError, logger as linux_logger, SymbolicFile class LinuxTest(unittest.TestCase): @@ -56,6 +57,44 @@ def test_stack_init(self) -> None: for i, env in enumerate(envp): self.assertEqual(cpu.read_string(cpu.read_int(envp_ptr + i * 8)), env) + def test_symbolic_file_wildcard(self) -> None: + with tempfile.NamedTemporaryFile("w") as fp: + # Write mixed symbolic and concrete data to our file + fp.write("++concrete++") + fp.flush() + + # setup logger for our assertion + prev_log_level = linux_logger.getEffectiveLevel() + linux_logger.setLevel(logging.DEBUG) + + with self.assertLogs(linux_logger, logging.DEBUG) as cm: + _ = SymbolicFile(ConstraintSet(), fp.name) + dmsg = "Found 4 free symbolic values" + self.assertIn(dmsg, "\n".join(cm.output)) + + with self.assertLogs(linux_logger, logging.DEBUG) as cm: + _ = SymbolicFile(ConstraintSet(), fp.name, wildcard="+", max_size=4) + dmsg = "Found 4 free symbolic values" + self.assertIn(dmsg, "\n".join(cm.output)) + + with self.assertLogs(linux_logger, logging.DEBUG) as cm: + _ = SymbolicFile(ConstraintSet(), fp.name, wildcard="+", max_size=2) + dmsg = "Found 4 free symbolic values" + wmsg = "Found more wildcards in the file than free symbolic values allowed (4 > 2)" + self.assertIn(wmsg, "\n".join(cm.output)) + + with self.assertLogs(linux_logger, logging.DEBUG) as cm: + _ = SymbolicFile(ConstraintSet(), fp.name, wildcard="|") + dmsg = "Found 0 free symbolic values" + self.assertIn(dmsg, "\n".join(cm.output)) + + with self.assertRaises(AssertionError) as ex: + _ = SymbolicFile(ConstraintSet(), fp.name, wildcard="Æ") + emsg = "needs to be a single byte" + self.assertIn(emsg, repr(ex.exception)) + + linux_logger.setLevel(prev_log_level) + def test_load_maps(self) -> None: mappings = self.linux.current.memory.mappings()