Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2

Static Driver Verifier (SDV) is a verification tool included in the Windows 7 Driver Kit (WDK). SDV uses SLAM as the program analysis engine. SDV 2.0 released with Windows 7 uses a re-designed SLAM2 engine. SLAM2 improves the precision and performance of predicate evaluation by using Z3 SMT solver. To handle predicates with pointers in SLAM2, we propose a novel set of axioms that defines a logical memory model, which is one of the underlying concepts and limitations of SLAM. We also designed an algorithm of encoding predicates passed to Z3 with uninterpreted functions over integers. In this paper, we present the axioms and the encoding. We also show how the axioms can be modified to achieve a better precision by refining the memory model. Our profiling of SDV runs on real device drivers confirms that the axioms and the encoding allowed SLAM2 to achieve a good balance between the precision required by the logical memory model, and Z3 performance on complex predicates. Our presentation of the axioms and the encoding in this paper is decoupled from SLAM2, such that they could be utilized by other static analysis tools when dealing with pointer predicates – often a bottleneck in such tools.