Example 3. Consider the implementation of f given in Figure 2,
and suppose we want to determine the condition under which
pointer p is dereferenced in f. It is easy to see that the exact condition for p’s dereference is given by the constraint:
p!=NULL Ù flag!=0 Ù buf!=NULL Ù *buf ==’i’
Since the return value of malloc (i.e., buf) and the user
input (i.e., *buf) are statically unknown, the strongest observable necessary condition for f to dereference p is given by the
simpler condition:
p!=NULL Ù flag!=0
On the other hand, the weakest observable sufficient condition
for the dereference is false, which makes sense because no
restriction on the arguments to f can guarantee that p is dereferenced. Observe that these strongest necessary and weakest
sufficient conditions are as precise as the original formula for
deciding whether p is dereferenced by f at any call site of f, and
furthermore, these formulas are much more concise than the
original formula.
4. SoLVinG The conSTRain TS
In this section, we now return to the problem of computing
strongest necessary and weakest sufficient conditions containing only observable variables for each Pa, fi, Cj from System
of Equations 1. Our algorithm first eliminates the choice variables from every formula. We then manipulate the system
to preserve strongest necessary (weakest sufficient) conditions under substitution (Section 4. 2). Finally, we solve the
equations to eliminate recursive constraints (Section 4. 3),
yielding a system of (nonrecursive) formulas over observable
variables. Each step preserves the satisfiability/validity of the
original equations, and thus the original may/must query can
be decided using a standard SAT solver on the final formulas.
4. 1. eliminating choice variables
To eliminate the choice variables from the formulas in
Figure 1, we use the following well-known result for computing strongest necessary and weakest sufficient conditions
for Boolean formulas4:
Lemma 1. The strongest necessary and weakest sufficient conditions of Boolean formula f not containing variable b are given by:
SNC (f, b) º f[true/b ] Ú f[false/b ]
WSC (f, b) º f[true/b ] Ù f[false/b ]
120 communicaTionS of The acm | auGust 2010 | Vol. 53 | no. 8
Since our definition of satisfiability and validity must also
take into account the implicit existence and uniqueness
conditions, this standard way of computing strongest nec-
essary and weakest sufficient conditions of Boolean formu-
las must be slightly modified. In particular, let b be a choice
variable to be eliminated, and let ψexist and ψunique represent
the existence and uniqueness conditions involving b. Then,
we compute strongest necessary and weakest sufficient con-
ditions as follows:
After applying these elimination procedures to the con-
straint system from Figure 1, we obtain two distinct sets of
equations of the form:
System of Equations 2.
ESC is analogous to ENC.
Example 4. Consider the function given in Example 1, for
which Boolean constraints are given in Example 2. We compute
the weakest sufficient condition for Pf, a, C1:
The reader can verify that the strongest necessary condition for
Pf, a, C1 is true. The existence and uniquencess constraints are
omitted since they are redundant.
4. 2. Preservation under substitution
Our goal is to solve the recursive system given in System
of Equations 2 by an iterative, fixed point computation. However, there is a problem: as it stands, System of
Equations 2 may not preserve strongest necessary and weakest sufficient conditions under substitution for two reasons:
• Strongest necessary and weakest sufficient conditions
are not preserved under negation (i.e., Ø⎡f⎤ ⎡Øf⎤ and
Ø ⎣f ⎦ ⎣Øf⎦ ), and the formulas from System of Equations
2 contain negated return (P) variables. Therefore, substituting ØP by Ø⎡P⎤ and Ø⎣P⎦ would yield incorrect necessary and sufficient conditions, respectively.
