[cfe-commits] [PATCH] Add Assumer class

[Ted Kremenek]

On Aug 26, 2008, at 4:01 AM, Zhongxing Xu wrote:

> The Assume interface is abstracted into a new class. It's not  
> finished. It's intended to replace current Assume() interface.
>
> -Zhongxing Xu
> <assume.patch>_______________________________________________
> cfe-commits mailing list
> cfe-commits at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits

Hi Zhongxing,

I think this is definitely a step in the right direction.  My plan was  
to refactor the "Assume" logic in GRStateManager.  I'm glad you're  
spearheading the effort.

Here are some comments!

First, I have to be honest that I don't like the name "Assumer" for  
the actual interface.  I think that using the word "Assume" is fine  
for the methods since that matches with the model-checking terminology  
(essentially, "Assume" represents a verb, or action, that we are  
taking with respect to modifying the state).  I think the name of the  
Assumer class should reflect what it represents, which are constraints  
on the values of state.  So I suggest *something* like the following  
(we can iterate on the precise name):

   Assumer ->  ConstraintsManager

This makes it much more clear that the ConstraintsManager manages  
'constraints' within the state.  We can iterate on the name, but  
"Assumer" I feel that isn't descriptive enough.

I also think this patch is a little incomplete, since the code it  
introduces doesn't actually get hooked up to GRState.  All of the  
Assume methods in GRStateManager should just forward over to the  
ConstraintManager object, e.g:

class GRStateManager {
   ...
   const GRState* Assume(const GRState* St, NonLVal Cond, bool  
Assumption,
                            bool& isFeasible) {
     return ConstraintsMgr.Assume(St, *this, Cond, Assumption,  
isFeasible);
}

If you actually migrate this core logic over to  
BasicConstraintsManager (BasicAssumer in your patch), then you can  
actually run "make test" to see if your patch does the right thing.

Afterwards, all the 'AddEQ' logic, etc., in GRState just gets moved  
over to BasicConstraintsManager.  This can be done in a second patch.   
AddEQ and friends can still be methods in GRState (if we need them),  
but they should just forward over to the methods in ConstraintsManager.

In another later patch, all the ConstEqTy and ConstNotEqTy logic in  
GRState.cpp should be also moved over to BasicConstaintsManager.  This  
means that ConstraintManager (or rather its subclasses) will also have  
to implement methods such as RemoveDeadSymbols (just like we do for  
Environment and StoreManager).

These changes will really factor out the symbolic reasoning of value  
constraints out of GRState.cpp into a separate module, which is a long  
needed change.

Ted