[cfe-commits] [PATCH] Expressions have lvalues and rvalues

[Ted Kremenek]

Hi Zhongxing,

I think you put these points very elegantly, and you nicely summarized  
the abstraction used in the static analyzer.  I've responded to your  
later email with some other points I want to mention.

Ted

On Oct 10, 2008, at 7:09 PM, Zhongxing Xu wrote:

> Hi Sebastian,
>
> I know where the confusion comes from: we are from two different  
> points of view. You are from pure programming language and compiler  
> point of view. I am from a mathematical interpretation of programs  
> point of view.
>
> In PL/compiler view, lvalue/rvalue is equivalent to an expression.  
> So we might be more explicit to directly say an lvalue expression or  
> rvalue expression. An lvalue expression is an expression refering to  
> an object in the memory (per C standard). So an lvalue expression is  
> an real object exists in memory. And the rest expressions are rvalue  
> expressions. This is very clear.
>
> But in static analysis, only having a programming language level  
> expression concept is not enough. We want to do interpretation of  
> programs and use some mathematics to reason about programs. So we  
> designed an interpretation model of programs as follows.
>
> Basically, we divide the things into 3 domains: language domain,  
> memory domain, mathematics domain. For an expression, we conceptly  
> view it as a 3-tuple.
>
> expression --- memory  ----- value
>
> The first expression represent the concept in the programming  
> language. It is a textual representation of the expression. In  
> clang, they correspond to numerous *Expr classes.
>
> Second, the expression (might) represents an object in memory. In  
> libAnalysis, we designed the region model for modeling memory.
>
> Third, the memory object stores a value. In libAnalysis, we use RVal  
> to abstractly represent this value.
>
> Note that, here the value is in the mathematical sense: it is a real  
> value, represented by bits in the memory.
>
> In this interpretation model, I redefined the concept lvalue and  
> rvalue slightly. I made them a property of expressions, not as  
> expressions themselves. I define the lvalue of an expression as the  
> memory address of the object it refering to, and rvalue of an  
> expression as the value it evaluates to when placed at the RHS of an  
> assignment (I don't have a better definition currently).
>
> All expressions have rvalue, because it should evaluate to some  
> value. But not all expressions have lvalue. Only expressions  
> refering memory objects have lvalue. For example, &x has no lvalue,  
> but has rvalue, which is x's lvalue.
>
> Now let's talk about where the LVal/NonLVal comes from. Look at the  
> above 3-tuple:
>
> expression -- memory -- value
>
> Remember we are doing static analysis, and we are going to use some  
> mathematics to analyze program. So what objects are we processing in  
> mathematics? They are the value in the memory, i.e. the value on the  
> rightmost of the tuple. Literally they are raw bits. But we made  
> them more abstract into RVal. Furthermore, we noticed that the most  
> essential distinction among these varous abstract values (RVals) is  
> that some of them are address value, some of them are not. So here  
> comes LVal and NonLVal. We use LVal to represent an abstract address  
> value, and NonLVal to represent an numerical value.
>
> So, LVal and NonLVal are used to represent the abstract values in  
> the mathmatical sense, that has nothing to do with expressions in  
> the programming language sense. We need these mathematical values in  
> our symbolic analysis of the program. They are conceptly values  
> stored in our simulated computer memory. They are in a different  
> world from C/C++ expressions.
>
> An expression's lvalue evaluates (through our interpretation) into a  
> LVal.
> An expression's rvalue evaluates (through our interpretation) into a  
> NonLVal (e.g. 2*x+3), or a LVal (e.g. &x).
>
> _______________________________________________
> cfe-commits mailing list
> cfe-commits at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits