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 language-agnostic framework that leverages runtime profiling to optimize constraint solving across different 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 15.9-85.2% reduction in constraint solving time across the benchmark suite while maintaining path coverage. EVP's modular design enables adoption by existing tools without architectural changes, establishing empirical profiling as a practical, engine-independent optimization for symbolic execution.