[cfe-commits] [PATCH] Add Assumer class

Zhongxing Xu xuzhongxing at gmail.com
Tue Aug 26 18:44:40 PDT 2008

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.

> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20080827/a70d2a28/attachment.html>

More information about the cfe-commits mailing list