com.surelogic
Annotation Type RegionEffects

@Documented
@Target(value={METHOD,CONSTRUCTOR})
public @interface RegionEffects

Declares the regions that may be read or written during execution of the method or constructor to which this annotation is applied. In general the annotation syntax is

@RegionEffects("reads readTarget , ... ; writes writeTarget, ... ")

The annotation contains reads and writes clauses that each have a list of one or more targets. The reads clause describes the data that may be read by the method/constructor; the writes clause describes the state that may be read or written by the method/constructor. Because writing includes reading, there is no need to list a target in the reads clause if its state is already described in the writes clause.

Both the reads and writes clauses are optional: to indicate that there are no effects use @RegionEffects("none"). An unannotated method is assumed to have the annotation @RegionEffects("writes All") which declares that the method could read from or write to any state in the program.

A target is an extrinsic syntactic mechanism to name references to regions, and can be one of

RegionName

If RegionName is an instance region, then it is the same as this:RegionName (see below). If RegionName is a static region, it must be a region declared in the annotated class or one of its ancestors, and is thus a short hand for pkg.C:RegionName below.

this:RegionName

RegionName is an instance region of the class containing the method.

param:RegionName

param is a parameter of the method that references an object. RegionName is a region of the class of param's type.

pkg.C.this:RegionName

pkg.C is an "outer class" of the class that contains the annotated method. That is, the method being annotated is in class D, and D is an inner class of C. Region is a region of pkg.C.

any(pkg.C):RegionName

The any instance target: pkg.C is a class name and RegionName is a region of pkg.C.

pkg.C:RegionName

The static target: RegionName is a static region of class pkg.C.

The analysis checks that the actual effects of the method implementation are no greater than its declared effects. There are several fine points to this:

• Uses of final fields produce no effects and do not need to be declared.
• Effects on local variables are not visible outside of a method/constructor and do not need to be declared.
• Effects on objects created within a method are not visible outside of a method and do not need to be declared.
• Constructors do not have to declare the effects on the Instance region of the object under construction.
• Region aggregation (see Unique and UniqueInRegion) is taken into account.

Semantics:

States the upper-bound effects of an annotated method or constructor on the Java heap. These effects do not include the stack of any thread. An implementation of a method or constructor is consistent with its declared RegionEffects if all possible executions read and write only to the state specified in the annotation.

At runtime, a target—like a region—represents a subset of the JVM heap, subdividing one or more objects in the heap. While in most cases a target is equivalent to particular runtime region, the any instance target refers to state that is not possible to name with any single region.

this:RegionName

The target denotes the runtime region RegionName of the object o referenced by the method/constructor's receiver.

param:RegionName

The target denotes the runtime region RegionName of the object o referenced by the parameter p at the start of the method's execution.

pkg.C.this:RegionName

The target denotes the runtime region RegionName of the object o referenced by the qualified receiver pkg.C.this.

any(pkg.C):RegionName

Let X be the set of all heap objects o such that o has type T and T instanceof pkg.C. The target denotes the union of the runtime regions RegionName of each o ∈ X

pkg.C:Region

The target denotes the runtime region of the static region RegionName declared in class pkg.C.

Examples:

Here is a simple "variable" class with effects annotations.

 @Region("public ValueRegion")
 public class Var {
 
   @InRegion("ValueRegion")
   private int value;
 
   @RegionEffects("none")
   public Var(int v) {
     value = v;
   }
 
   @RegionEffects("reads ValueRegion")
   public int getValue() {
     return value;
   }
 
   @RegionEffects("writes ValueRegion")
   public void setValue(int v) {
     value = v;
   }
 }
 

Javadoc usage notes:

This annotation may placed in Javadoc, which can be useful for Java 1.4 code which does not include language support for annotations, via the @annotate tag.

 /**
  * @annotate Region("public ValueRegion")
  */
 public class Var {
 
   /**
    * @annotate InRegion("ValueRegion")
    */
   private int value;
 
   /**
    * @annotate RegionEffects("none")
    */
   public Var(int v) {
     value = v;
   }
 
   /**
    * @annotate RegionEffects("reads ValueRegion")
    */
   public int getValue() {
     return value;
   }
 
   /**
    * @annotate RegionEffects("writes ValueRegion")
    */
   public void setValue(int v) {
     value = v;
   }
 }
 

Required Element Summary

String

value This attribute is either "none" to indicate that the method/constructor has no visible effects or divided into separate (and optional) reads and writes clauses.

Element Detail

value

public abstract String value

This attribute is either "none" to indicate that the method/constructor has no visible effects or divided into separate (and optional) reads and writes clauses. Each clause is a list of comma-separated targets describing the regions that may be read/written. The clauses are separated by a semicolon.

Examples:

 @RegionEffects("reads this:Instance; writes other:Instance")
 @RegionEffects("writes C:StaticRegion, any(D):Instance; reads this:Instance")
 @RegionEffects("reads this:Instance")
 @RegionEffects("writes this:Instance")
 @RegionEffects("none")
 

The value of this attribute must conform to the following grammar (in Augmented Backus–Naur Form):

 value =
   none /  ; No effects
   readsEffect [";" writesEffect] /
   writesEffect [";" readsEffect]
 
 readsEffect = "reads" effectsSpecification
 
 writesEffect = "writes" effectsSpecification
 
 effectsSpecification = "nothing" / effectSpecification *("," effectSpecification)
   
 effectSpecification =
   simpleEffectExpression ":" simpleRegionSpecification /
   IDENTIFIER   ; instance region of "this" or a static region declared in the current class or one of its ancestors 
 
 simpleEffectExpression =
   "any" "(" namedType ")" /    ; any instance
   namedType "." "this" /       ; qualified this expression
   namedType /                  ; class name 
   simpleExpression             ; parameter name
 
 namedType = IDENTIFIER *("." IDENTIFIER)
 
 simpleExpression = "this" / IDENTIFIER
 
 simpleRegionSpecification = IDENTIFIER  ; Region of the class being annotated
 
 IDENTIFIER = Legal Java Identifier