Profile-Guided Constraint Simplification for Symbolic Execution

Constraint solving remains the primary bottleneck in symbolic execution, consuming up to 90% of analysis time. We present EVP (Empirical Value Profiling), a framework that leverages runtime profiling to optimize constraint solving within LLVM-based symbolic execution engines. EVP identifies program variables that consistently assume limited sets of concrete values during execution, then provides this information through a standardized API that symbolic executors can use to simplify constraints. Our framework consists of three decoupled components: (1) an LLVM-based profiler that tracks variable values at branch points, (2) a value analyzer that identifies limited-domain variables using configurable thresholds, and (3) a constraint simplification API that integrates with any SMT-based symbolic executor. We demonstrate EVP’s generalizability by integrating it with KLEE, achieving a 12.4-85.2% reduction in constraint-solving time across the benchmark programs while maintaining minimal trade-offs. EVP’s modular design enables adoption by existing tools without major architectural changes, establishing empirical profiling as a practical optimization for symbolic execution.