[cfe-commits] [PATCH] Add Assumer class

[Ted Kremenek]

On Aug 26, 2008, at 6:44 PM, Zhongxing Xu wrote:

>
>
> On Wed, Aug 27, 2008 at 1:04 AM, Ted Kremenek <kremenek at apple.com>  
> wrote:
>
> On Aug 26, 2008, at 4:01 AM, Zhongxing Xu wrote:
>
> 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 agree.
>
>
>
> 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
>
> I know. I sent this incomplete one just to get your feedback. Now I  
> know I'm in the right direction and what to do next.

Okay!

>
>
>
>
> 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
>
> Totally agree.

Sounds great!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20080826/92c5f479/attachment.html>