<div dir="ltr"><br><br><div class="gmail_quote">On Wed, Aug 27, 2008 at 1:04 AM, Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com">kremenek@apple.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="Ih2E3d"><br>
On Aug 26, 2008, at 4:01 AM, Zhongxing Xu wrote:<br>
</div><br>
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):<br>

<br>
  Assumer ->  ConstraintsManager<br>
<br>
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.</blockquote><div><br>
I agree.<br> </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><br>
<br>
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</blockquote>
<div><br>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.<br> </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>
<br>
class GRStateManager {<br>
  ...<br>
  const GRState* Assume(const GRState* St, NonLVal Cond, bool Assumption,<br>
                           bool& isFeasible) {<br>
    return ConstraintsMgr.Assume(St, *this, Cond, Assumption, isFeasible);<br>
}<br>
<br>
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.<br>
<br>
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.<br>

<br>
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).<br>

<br>
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.<br><font color="#888888">
<br>
Ted<br>
</font></blockquote></div><br>Totally agree.<br></div>