A systematic representation of path constraints for implicit path enumeration technique

Accuracy of implicit path enumeration technique (IPET), which statically estimates the worst-case execution time of a program using integer linear programming, relies on flow information captured as flow facts. Unfortunately, flow facts are inadequate for capturing complex and often subtle path constraints such as causalities. Manual annotation often introduces many disjunctions, and performance of IPET computation suffers significantly. This paper proposes a technique of encoding a subset of path constraints into flow facts. The technique has advantages over conventional approaches: (1) translation process is fully automated and (2) efficient IPET computation is possible because generated flow facts are compact in that they contain at most one disjunction. To demonstrate the effectiveness of our technique, a software tool was implemented to automatically generate flow facts for the subset of path constraints and case study has been conducted using public benchmark suites, GNU openSSH codes, and Korea multi-purpose satellite (KOMPSAT-1) software.