[sv-ac] 1678 name resolution and the rewriting algorithm of 1549

Hi Folks:

In 1549, we introduced a local variable declaration notation 
in the abstract syntax.

In revising the rewriting algorithm, I deleted the parts about
making local variable names unique.  The rules for overshadowing
in 1549 make this unnecessary in some cases.  Doron asked about
this, but I seemed to convince him that the overshadowing took 
care of the problems.

However, 1678 points out that a naive treatment of local variable
identifiers results in name resolution issues when local variables are
passed as actual arguments to other instances.  The overshadowing
mechanism of 1549 does not take care of this problem.

I do not think that this problem is specific to local variables.  When
rewriting and substituting actual arguments, we must respect name
resolution.  Simply looking at the identifiers, references,
etc. written in the source code is not good enough.  There can be
incorrect aliasing for all sorts of things other than local variables.

In order to resolve 1678, I think we need to add some language
(hopefully a small amount) to say that name resolution still needs to
be taken care of properly when following the rewriting algorithm.

Name resolution is not something that we should be trying to capture
in Annex F, so I don't think we should make a special point about
making local variable identifiers unique.  That would give the wrong
impression that other references do not also need to be accounted for
with care.

I have uploaded to Mantis 1678 and attached below an example of
carrying out the rewriting algorithm while paying attention to name
resolution.  I don't envision it being added to the LRM.

J.H.


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.


---------------------------------------------------------------------------------------
2007-11-02

The example in the Mantis description is the following:

   A naive interpretation of substitution may lead to local variables
   name clashing.
   
   Here is an example of name clashing.
   
   sequence r1(lv);
      logic [7:0] lv1;
      (a, lv1 = 0) 
      ##1 (!a, lv1 = lv1 + lv)[*0:$] 
      ##1 a 
      ##0 (1, lv = lv1);
   endsequence
   
   sequence r2;
      logic [7:0] lv1;
      (b, lv1 = c) 
      ##1 r1(lv1)
      ##1 (lv1 == d);
   endsequence
   
   
   A naive substitution will result in the following:
   
   sequence r2;
      logic [7:0] lv1;
      logic [7:0] lv1;
      (b, lv1 = c) 
      ##1 (a, lv1 = 0) 
      ##1 (!a, lv1 = lv1 + lv1)[*0:$] 
      ##1 a 
      ##0 (1, lv1 = lv1)
      ##1 (lv1 == d);
   endsequence
   
   
   What we really want is to rename lv1 in r1 to a unique name before the
   substitution occurs. Then we get
   
   sequence r2;
      logic [7:0] lv1;
      logic [7:0] unique_lv1;
      (b, lv1 = c) 
      ##1 (a, unique_lv1 = 0) 
      ##1 (!a, unique_lv1 = unique_lv1 +lv1)[*0:$] 
      ##1 a 
      ##0 (1, lv1 = unique_lv1)
      ##1 (lv1 == d);
   endsequence


1549 has added local variables to the abstract syntax, and this is
used as a part of the rewriting algorithm.  

The rewriting algorithm applied to this example will not resolve the
conflict if the naive treatment of the colliding identifiers lv1 is 
handled in the same way as above.

The original suggestion from the argument subcommittee and in the description 
of 1678 is to make the local variable identifiers unique. 

Distinguishing the colliding local variable identifiers must be done, but I
do not think it is the full solution.

Local variables are not special in requiring respect of rules of name
resolution.  Every identifier, reference, etc. has to be treated
appropriately to avoid incorrect aliasing or collisions.  Tools must
already deal with this on a broad scale in order to elaborate
correctly.

We need to make sure that it is understood that the rewriting algorithm
is not intended to account for name resolution details.  Those are assumed
to be taken care of, not just for local variables, but for all identifiers,
references, etc.  If we make special mention of making local variable identifiers
unique we will give the wrong impression.

The unique_lv1 added above is an example of accounting for name resolution
that only payes attention to the local variables.  The example is 
simple enough that no other collisions are possible.  

Let's try to run the rewriting algorithm in a way that suggests a more
general treatment of name resolution.

Let us consider \varpi to be an instance of r2.  For name resolution, call
this instance r2\inst, so \varpi = r2\inst.

a. According to the algorithm, we need to consider the context of r2\inst.  
   Depending, we replace r2\inst by either
   
      item(sequence'flatten_sequence(r2\inst))
   
   or
   
      flatten_sequence(r2\inst)
   
   Everything interesting is happening in flatten_sequence(r2\inst), so this 
   distinction is not important.  For simplicity of exposition, let's assume 
   that this step to replace \varpi by flatten_sequence(r2\inst).
   
b. flatten_sequence(r2\inst).1 says to create a copy r2' of the declaration of 
   r2\inst.  The understanding is that r2' is a new name to talk about this 
   copy.  It should not collide with any other name for anything.
 
   For name resolution, a local variable is local to this copied declaration, but
   the copied declaration should resolve other references the same way the original
   r2 did.  The suffixes after \ are supposed to represent additional information 
   being used to get proper name resolution:
   
      sequence r2';
         logic [7:0] lv1\r2';
         (b\r2, lv1\r2' = c\r2) 
         ##1 r1\r2(lv1\r2')
         ##1 (lv1\r2' == d\r2);
      endsequence
    
c. There is nothing to do for flatten_sequence(r2\inst).2-5 since r2' has no formal 
   argument.
   
d. flatten_sequence(r2\inst).6 says to return 
   
      (
         logic [7:0] lv1\r2';
         (b\r2, lv1\r2' = c\r2) 
         ##1 r1\r2(lv1\r2')
         ##1 (lv1\r2' == d\r2);
      )
   
   so this is our new \varpi.
   
e. Now we must replace the instance r1\r2(lv1\r2') of r1 in \varpi by 
   flatten_sequence(r1\r2(lv1\r2')).  I am assuming that r1\r2(lv1\r2') 
   unambiguously identifies the instance in \varpi.

f. flatten_sequence(r1\r2(lv1\r2')).1 says to create a copy r1' of the declaration 
   of r1:
  
      sequence r1'(lv\r1');
         logic [7:0] lv1\r1';
         (a\r1, lv1\r1' = 0) 
         ##1 (!a\r1, lv1\r1' = lv1\r1' + lv\r1')[*0:$] 
         ##1 a\r1 
         ##0 (1, lv\r1' = lv1\r1');
      endsequence

g. flatten_sequence(r1\r2(lv1\r2')).2 says to define a_{lv\r1'} to be lv1\r2'.

h. lv\r1' is an untyped formal argument of r1'.  a_{lv\r1'} is not $.  Therefore, 
   flatten_sequence(r1\r2(lv1\r2')).3 says to replace each reference to lv\r1' in r1'
   with either (lv1\r2') or lv1\r2', depending on whether adding the parentheses is
   legal.  This gives

      sequence r1'(lv\r1');
         logic [7:0] lv1\r1';
         (a\r1, lv1\r1' = 0) 
         ##1 (!a\r1, lv1\r1' = lv1\r1' + (lv1\r2'))[*0:$] 
         ##1 a\r1 
         ##0 (1, lv1\r2' = lv1\r1');
      endsequence


i. There are no typed formal arguments, so nothing needs to be done for
   flatten_sequence(r1\r2(lv1\r2')).4-5.

j. flatten_sequence(r1\r2(lv1\r2')).6 says to return 

      (
         logic [7:0] lv1\r1';
         (a\r1, lv1\r1' = 0) 
         ##1 (!a\r1, lv1\r1' = lv1\r1' + (lv1\r2'))[*0:$] 
         ##1 a\r1 
         ##0 (1, lv1\r2' = lv1\r1')
      )


k. Substituting this in for r1\r2(lv1\r2') in \varpi gives

      \varpi = 
      (
         logic [7:0] lv1\r2';
         (b\r2, lv1\r2' = c\r2) 
         ##1 
         (
            logic [7:0] lv1\r1';
            (a\r1, lv1\r1' = 0) 
            ##1 (!a\r1, lv1\r1' = lv1\r1' + (lv1\r2'))[*0:$] 
            ##1 a\r1 
            ##0 (1, lv1\r2' = lv1\r1')
         )
         ##1 (lv1\r2' == d\r2);
      )