<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On Oct 11, 2008, at 8:16 PM, Zhongxing Xu wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 14px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0; "><div class="gmail_quote">On Sun, Oct 12, 2008 at 11:14 AM, Zhongxing Xu<span class="Apple-converted-space"> </span><span dir="ltr"><<a href="mailto:xuzhongxing@gmail.com">xuzhongxing@gmail.com</a>></span><span class="Apple-converted-space"> </span>wrote:<br><blockquote class="gmail_quote" style="border-left-width: 1px; border-left-style: solid; border-left-color: rgb(204, 204, 204); margin-top: 0pt; margin-right: 0pt; margin-bottom: 0pt; margin-left: 0.8ex; padding-left: 1ex; "><div dir="ltr"><div class="gmail_quote"><div class="Ih2E3d"><blockquote class="gmail_quote" style="border-left-width: 1px; border-left-style: solid; border-left-color: rgb(204, 204, 204); margin-top: 0pt; margin-right: 0pt; margin-bottom: 0pt; margin-left: 0.8ex; padding-left: 1ex; ">So how about calling them Address and NonAddress? This would get rid of the dangerous similarity between LVal and LValue.<br><font color="#888888"><br>Sebastian</font></blockquote></div><div><br>What about LocVal and NonLocVal?<span class="Apple-converted-space"> </span><br></div></div><br></div></blockquote></div><br>How about:<br><br>RVal => AVal (abstract value)<br>LVal => LocVal (location value)<br>NonLVal => NonLocVal (non-location value)</span></blockquote></div><br><div>Sounds good, other than "AVal" should probably be something like "AbstractVal", since we don't use it that much and the "A" doesn't really mean anything unless you look at the comments (can't use "Abs" because someone might think it means "absolute"). ExprVal is also a possibility (see later in this email for more comments).</div><div><br></div><div>Getting back to the points both you and Sebastian made, I'm wondering if there is any advantage with changing the implementation of RVal/LVal to be something much closer to the way C++ reasons about these concepts. This might in the long run clean up a whole bunch of things, especially as we add more support for C++.</div><div><br></div><div>I don't have any concrete ideas, but there exists a lot of redundancy between the lval and nonlval classes. For example, lval::ConcreteInt and nonlval::ConcreteInt are essentially the same class representing the same data. The same goes for lval::SymbolVal and nonlval::SymbolVal. The distinction between the lval:: and nonlval:: versions is purely context, which is often redundant since one often (always?) knows the current context and how these values should be interpreted. If we modeled lvalues in the sense that Sebastian articulated, we would probably only have a handful of classes: lval::MemoryRegion, lval::Undefined, lval::Unknown, and that's probably it. We would have an nonlval::MemoryRegion (or rather rval::MemoryRegion if we want nonlval to represent rvalues), but symbols, integers, etc., would always be rvalues.</div><div><br></div><div>One thing about this is that it makes the transfer function structure basically fall out from what's in the C/C++ standards. For example, the '*' operator essentially has the following type signature:</div><div><br></div><div>* : rval -> lval</div><div><br></div><div>Similarly, references to variables and the '&' operator could be represented as follows:</div><div><br></div><div>variable reference: (declrefexpr) -> lval</div><div>& : lval -> rval (with the rval being an rval::MemoryRegion)</div><div><br></div><div>In contexts where an lval is used as an rval, we have an implicit conversion (as stated in the C++ standard). Such implicit conversations would be represented by a transfer function, which cause a new state and ExplodedNode to be created to represent the effect of this conversion. For example, an implicit conversion from an lval to rval could result in a value load (e.g., EvalLoad, which would have the type signature lval -> rval).</div><div><br></div><div>Zhongxing: In a roundabout way, I think your patch (which I have now looked at) is trying to resolve some of the confusion between rvalues and lvalues, but I'm wondering if the distinction between rvalues and lvalues really should happen in the Store. This of course is a naturally progression of the current design, but after Sebastian's points I'm wondering if that is the right direction. In my mind, all the store should care about is the mapping between regions and abstract values (a notion that has nothing to do with LVal and NonLval) and the mapping between variable names and the their regions. These are pretty clean interfaces that don't have to get tangled with the notion of rvalues and lvalues, which seem more related to how GRExprEngine should handle individual expressions.</div><div><br></div><div>In a nutshell, I'm wondering if we should do the following:</div><div><br></div><div>1) Change "RVal" to "ExprVal" (representing the value of an expression). ExprVal makes it clear that these objects represent the evaluation of an expression.</div><div><br></div><div>2) Change 'nonlval::" to "rval::", and remove most of the lval classes such as lval::SymbolicInt and lval::ConcreteInt. Add an "rval::MemoryRegion" class that mirrors "lval::MemoryRegion".</div><div><br></div><div>3) Change GRExprEngine to reason about rvals (rvalues) and lvals (lvalues) in the same way the C++ standard does. This is a big task, but I think it is mainly code restructuring. Loads would be handled as transfer functions (i.e., EvalLoad) doing the implicit conversions between lvals -> rvals.</div><div><br></div><div>I see three advantages of these changes:</div><div><br></div><div>1) The structure of GRExpEngine more closely reflects the semantics of C/C++ as given by the respective standards. This will make the analyzer much easier to extend potential C++ 0X features, such as rvalue references, as the design of how to implement these features in GRExprEngine should be more obvious and intuitive. This should also address Sebastian's original concerns (and the concerns of those with a similar perspective). It will also make it much clearer for those new to the libAnalysis/GRExprEngine about what is going on.</div><div><br></div><div>2) There will probably be a significant code reduction/simplification in many cases, as the code duplication for lval::SymbolicVal and nonlval::SymbolicVal, lval::ConcreteInt and nonlval::ConcreteInt, gets eradicated.</div><div><br></div><div>3) The meaning/purpose of LVal/RVal/NonLval (whatever we call them) will be made clear: they exist purely for GRExprEngine to correctly implement/call the right transfer functions. The Environment class will be a mapping from "Expr* -> ExprVal", and implementations of the Store won't care about ExprVals at all; just regions and the values they map to. I see this as a being a huge conceptually cleanup; implementations of Store won't have to reason about rvalues and lvalues at all, just locations and the values stored at those locations. The distinction between rvalues and lvalues is something that C and C++ language lawyers should care about, but people wishing to model the heap in a particular implementation of store shouldn't have to care about these things at all.</div><div><br></div><div>What do you think? It seems like important changes like this (if we make them) should get in before the system gets any larger and more complex. Note that I don't think these changes are necessarily the best ones; I'm just very much interested in discussing whether or not the overall design of RVals/Lvals needs to be changed.</div><div><br></div><div>Ted</div></body></html>