Linux binary symbolic execution not exploring multiple paths

[dguido]

Bug: Linux binary symbolic execution not exploring multiple paths

Summary

The examples/linux/basic example only generates 1 test case instead of the expected 2. The symbolic execution is not exploring both branches of a simple conditional statement.

Environment

• Manticore version: Latest master (commit 289e1e9)
• Python version: 3.11
• OS: Ubuntu Linux
• Installation method: uv pip install -e .

Steps to Reproduce

cd examples/linux
make  # Build the examples
manticore basic  # Or: python -m manticore basic

Expected Behavior

According to the comments in basic.c, Manticore should generate 2 test cases:

1. One where the input is <= 0x41
2. One where the input is > 0x41

The example documentation shows:

Expected output:
  $ manticore basic
  ...
  Generating testcase No. 1 for state No.3 - Program finished correctly
  Generating testcase No. 2 for state No.5 - Program finished correctly

Actual Behavior

Only 1 test case is generated:

$ python -m manticore basic
2025-08-23 03:56:50,529: [2202666] m.n.manticore:INFO: Loading program basic
...
2025-08-23 03:56:59,867: [2202666] m.c.manticore:INFO: Generated testcase No. 0 - test
2025-08-23 03:56:59,988: [2202666] m.c.manticore:INFO: Results in /root/manticore/examples/linux/mcore_kek0chbm

The generated test case has empty stdin and no constraints in the SMT file.

Root Cause Analysis

Issue 1: stdin not being attached to state

The investigation revealed that platform.input is not properly initialized with symbolic stdin. When checking the initial state:

m = Manticore.linux('./basic', stdin_size=256)
state = m._load(m._ready_states[0])
print(f"Has stdin: {hasattr(state.platform, 'stdin')}")  # Prints: False

The stdin should be attached via platform.input.write() in _make_linux() (manticore/native/manticore.py:503), but the platform doesn't have the expected stdin attribute.

Issue 2: Execution terminates early

The program terminates at the entry point (0x4017c0) without executing any instructions:

• No hooks are triggered
• No symbolic values are created
• No state forking occurs

Investigation Details

Test 1: Manual execution works correctly

$ printf "\x00\x00\x00\x00" | ./basic
Message: It is less than or equal to 0x41

$ printf "\x42\x00\x00\x00" | ./basic  
Message: It is greater than 0x41

Test 2: No symbolic values detected

Created debug scripts that hook various points in execution:

• Read syscall (0x41a020)
• After read (0x401717)
• Comparison instruction (0x40171d)
• Conditional jump (0x401722)

None of these hooks are ever triggered, indicating execution never reaches the main function.

Test 3: No state forking occurs

Monitoring for will_fork_state events shows zero forks throughout execution.

Test 4: Generated test case analysis

• test_00000000.stdin: Empty file (0 bytes)
• test_00000000.smt: Only declares STDIN variable, no constraints
• test_00000000.input: Shows all zeros for stdin

Code References

• Binary source: examples/linux/basic.c
• Manticore Linux loader: manticore/native/manticore.py:450-504
• Platform initialization: manticore/platforms/linux.py

Possible Regression

This appears to be a regression as the example documentation shows it previously worked. Recent commits that might be related:

• 1d3251f: Fix gzip state serialization Ubuntu 24.04 Python 3.12
• 882382c: Modernize package build configuration

Workaround

None found. The issue prevents basic symbolic execution functionality from working.

Reproducible Test Case

Created a minimal test that confirms the issue:

# Even this simple program only generates 1 state instead of 2
code = """
#include <unistd.h>
#include <stdio.h>

int main() {
    char c;
    if (read(0, &c, 1) \!= 1) return 1;
    if (c == 'A') {
        printf("Path A\\n");
    } else {
        printf("Path B\\n");  
    }
    return 0;
}
"""
# Compile with gcc -static, run with Manticore
# Expected: 2+ states
# Actual: 1 state

Impact

• Severity: Critical - Core functionality broken
• Affects all Linux binary symbolic execution
• Examples and tutorials don't work as documented
• New users cannot follow the quickstart guide
• Breaks fundamental symbolic execution capability