Fix incorrect comparison for symbolic file wildcards (#2454)

* Add tests for symbolic file wildcard handling

* Add example script and assertions for fileio.c in `examples` directory

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))

manticore/platforms/linux.py

@@ -474,6 +474,13 @@ class SymbolicFile(File):
         """
         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 @@ class SymbolicFile(File):
 
         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

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
 }
 

tests/native/test_integration_native.py

@@ -287,12 +287,6 @@ class NativeIntegrationTest(unittest.TestCase):
         """
         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.

tests/native/test_linux.py

@@ -1,4 +1,5 @@
 import errno
+import logging
 import unittest
 from binascii import hexlify
 
@@ -10,11 +11,11 @@ import re
 
 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 @@ class LinuxTest(unittest.TestCase):
         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()