[cfe-commits] r61147 - in /cfe/trunk: lib/Analysis/CFRefCount.cpp test/Analysis/uninit-vals-ps.c

[Ted Kremenek]

On Mar 10, 2009, at 12:40 AM, Zhongxing Xu wrote:

>
> I see your point. But how can we recognize which casts are semantic  
> changes and which are sugar typed?
> I doubt there is a consistent rule for this.
>

I'm fairly certain there is a consistent rule for this.  Actually, it  
is very simple: semantic changes due to type views on regions occur  
when the view would result in the chunk of memory being interpreted  
differently.  In the case of typedefs, they are just sugar for the  
underlying type, and don't change the semantics.

I've worked out a simple example to explain a proposal I have for  
possibly dealing with this issue.  The basic rules are as follows:

(a) Symbolic regions potentially don't have types other than "void*".   
That is, they are just chunks of memory.

(b) We "canonicalize" regions when performing bindings to them, but  
don't need to canonicalize regions when they are used as values for  
expressions (see example below).

(c) We strip away type views when performing pointer comparisons.  The  
type-checking in the frontend will tell us whether or not a pointer  
comparison is legal.

Here is my example.  There are other cases to consider, such as how to  
handle Objective-C and C++ objects, but I think this is a good  
starting point:


typedef struct s* MyPointer;
void* foo(void);

    void bar(void) {
1.   MyPointer q = foo();
2.   void *r = q;
3.   struct s* p = r;
4.   if (p == q)
5.      q->f = 10;
6.   if (q->f == 10)
         ...
7.   if (p->f == 10)
    }


What happens:

(a) On line 1 'foo()' evaluates to SymbolicRegion(Sym0).

(b) On line 1 the value of (a) is then casted to
     TypedViewRegion(MyPointer, SymbolicRegion(Sym0)).

(c) On line 1 that value is bound to 'q'.  Internally it is stored as
     'q' => TypedViewRegion(MyPointer, SymbolicRegion(Sym0)).  Observe  
that the
     typedef is retained as it is used as a value in the binding and  
not the key.

     Note that the syntax:

      'q' => some value

     is shorthand for

       VarRegion('q') => some value

(d) On line 2 we perform a load from 'q' (i.e., VarRegion('q')) to get  
the value
     TypedViewRegion(MyPointer, SymbolicRegion(Sym0)).

(e) On line 2 we cast (d) to void*.  This results
     in stripping the 'TypedViewRegion' and getting  
'SymbolicRegion(Sym0)'.  This
     value is directly bound to 'r' to get the binding
    'r' => SymbolicRegion(Sym0).

(f) On line 3 we load from 'r' to get SymbolicRegion(Sym0).

(g) On line 3 we cast (f) to 'struct s*', leaving us with the region
     TypedViewRegion(struct s*, SymbolicRegion(Sym0)).

(h) On line 3 we bound the value of (g) to 'p'.  This leaves us with the
     binding 'p' => TypedViewRegion(struct s*, SymbolicRegion(Sym0)).

(i) On line 4 we load both p and q, getting the values
      TypedViewRegion(struct s*, SymbolicRegion(Sym0)) (for 'p') and
      TypedViewRegion(MyPointer, SymbolicRegion(Sym0)) (for 'q').

    We then do a pointer comparison by erasing their "views" and see  
if they
    refer to the same memory object.  This means getting the first  
"non-view"
    ancestor region.  In this case, the ancestor region is  
SymbolicRegion(Sym0)
    in both cases.  This causes 'p == q' to evaluate to true.

    The rationale behind this view-stripping is that we are just  
comparing
    pointer addresses at this point, and "views" reason about the  
interpretation
    of the bytes within a region but not the address of the region  
itself.

    The "base region" doesn't have to be a SymbolicRegion. For example  
it could
    be a VarRegion.

(j) On line 5 we evaluate the l-value of 'q->f'.  This value is
     FieldRegion('f',TypedViewRegion(MyPointer, SymbolicRegion(Sym0))).

(k) On line 5 we ask the store manager to store '10' to the l-value  
computed
     at (j).  Internally, within the StoreManager, we translate:

       FieldRegion('f',TypedViewRegion(MyPointer,  
SymbolicRegion(Sym0))).

     to:

       FieldRegion('f',TypedViewRegion(struct s*,  
SymbolicRegion(Sym0))).

     and then bind '10' to the latter.

     Here we have "de-sugared" the TypedViewRegion so that all  
typedefs are
     translated to the underlying type.

     The rationale for this de-sugaring is that we want to  
"canonicalize" the key
     (and *not* the value) in the binding. This makes retrievals from  
the store
     easy in the presence of typedefs (which don't change the  
semantics of how a
     region is interpreted).

(l) One line 6 we compute the l-value of 'q->f' to be
     FieldRegion('f',TypedViewRegion(MyPointer,SymbolicRegion(0))) and  
then ask
     the store manager to load from that region.

     Within the StoreManager, the key is again canonicalized to
     FieldRegion('f',TypedViewRegion(struct s*, SymbolicRegion(0))).

     The retrieval from the store then uses this key, getting the  
value 10.

(m) Similarly, on line 7 we compute the l-value of 'p->f' to be
     FieldRegion('f',TypedViewRegion(struct s*, SymbolicRegion(0)))  
and then ask
     the store manager to load from that region.

     Within the StoreManager that key is also canonicalized, but since  
it is
     already canonical we just do the load.