  Quantitative program analysis involves computing numerical quantities about
individual or collections of program executions. An example of such a
computation is quantitative information flow analysis, where one estimates the
amount of information leaked about secret data through a program's output
channels. Such information can be quantified in several ways, including channel
capacity and (Shannon) entropy. In this paper, we formalize a class of
quantitative analysis problems defined over a weighted control flow graph of a
loop-free program. These problems can be solved using a combination of path
enumeration, SMT solving, and model counting. However, existing methods can
only handle very small programs, primarily because the number of execution
paths can be exponential in the program size. We show how path explosion can be
mitigated in some practical cases by taking advantage of special branching
structure and by novel algorithm design. We demonstrate our techniques by
computing the channel capacities of the timing side-channels of two programs
with extremely large numbers of paths.
