Symbolic Types for Lenient Symbolic Execution.
Stephen Chang, Alex Knauth, Emina Torlak.
45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018), Los Angeles, CA, USA, January 2018 (to appear).
[ pdf | code repo | artifact instructions, VirtualBox image (2.2GB) ]
We present lambda_sym, a typed lambda-calculus for lenient symbolic execution, where some language constructs do not recognize symbolic values. Its type system, however, ensures safe behavior of all symbolic values in a program. Our calculus extends a base occurrence typing system with symbolic types and mutable state, making it a suitable model for both functional and imperative symbolically executed languages. Naively allowing mutation in this mixed setting introduces soundness issues, however, so we further add concreteness polymorphism, which restores soundness without rejecting too many valid programs. To show that our calculus is a useful model for a real language, we implemented Typed Rosette, a typed extension of the solver-aided Rosette language. We evaluate Typed Rosette by porting a large code base, demonstrating that our type system accommodates a wide variety of symbolically executed programs.
Artifact Instructions |