1 @LATTICE("testL<testM,testM<testH")
2 @METHODDEFAULT("methodL<methodH,methodH<methodT,THISLOC=methodT,GLOBALLOC=methodT")
5 @LOC("testH") int fieldH;
6 @LOC("testM") int fieldM;
7 @LOC("testL") int fieldL;
8 @LOC("testM") Foo fooM;
9 @LOC("testH") static int globalH;
10 @LOC("testH") static Foo globalFoo;
11 @LOC("testH") static final String finalValue="FINAL";
14 public static void main (@LOC("methodH") String args[]){
15 @LOC("methodH") test t=new test();
20 @LOC("methodH") int localH; // LOC=[local.methodH]
21 fooM=new Foo(); // LOC=[local.methodT, field.testM]
24 // here, callee expects that arg1 is higher than arg2
25 // so caller should respects callee's constraints
26 fooM.doSomethingArgs(fieldH,fieldM);
33 public void methodInvoke(){
34 @LOC("methodH") Foo foo=new Foo();
36 // callee doesn't have any ordering constrints in-between method parameters.
37 // so the below cases are okay
38 foo.unrelatedTwoParams(fieldH,fieldL);
39 foo.unrelatedTwoParams(fieldL,fieldH);
43 @LOC("methodH,test.testL") int localVarL;
44 // value flows from the field [local.methodH,field.testH]
45 // to the local variable [local.methodL]
50 @LOC("methodT,test.testL")int localVar=fooM.a+fooM.b;
51 // GLB(fooM.a,fooM.b)=LOC[methodT,testM,FB]
52 // LOC[lovalVar]=[methodT,testL] < GLB(fooM.a,fooM.b)
55 // creating composite location by object references
57 @LOC("methodT,test.testM,Foo.FC,Bar.BB") int localVar=fooM.bar.a;
58 //LOC(fooM.bar.a)=[methodT,testM,FC,BA]
59 //localVar can flow into lower location of fooM.bar.a
60 fooM.bar.c=localVar; //[methodT,testM,FC,BB] < [methodT,testM,FC,BA]
63 // method has its own local variable lattice
64 @LATTICE("mL<mH,THISLOC=mH")
65 public void doOwnLattice(){
72 @LATTICE("mL<mH,THISLOC=mH")
73 public void doDelta(){
74 @LOC("DELTA(mH,test.testH)") int varDelta;
75 // LOC(varDelta) is slightly lower than [mH, testH]
77 @LOC("DELTA(DELTA(mH,test.testH))") int varDeltax2;
78 // applying double delta to [mH,testH]
80 varDelta=fieldH; // [mH,testH] -> DELTA[mh,testH]
81 varDeltax2=varDelta; //DELTA[mh,testH] -> DELTA[DELTA[mh,testH]]
83 fieldM=varDeltax2; // DELTA[DELTA[mh,testH]] -> [mH,testM]
86 @LATTICE("mL<mSpin,mSpin<mH,mSpin*")
87 public void doSpinLoc(){
88 // if loc is defined with the suffix *,
89 //value can be flowing around the same location
92 @LOC("mSpin") int varSpin;
97 // value can be flowing back to the varSpin
98 // since 'varSpin' is location allowing value to move within
99 // the same abstract location
100 varSpin=varSpin+varH;
105 @LATTICE("mL<mH,THISLOC=mL")
106 public void doSpinField(){
107 //only last element of the composite location can be the spinning loc
112 @LOC("mH") Bar localBar=new Bar();
114 localBar.b2=localBar.b1;
115 // LOC(localBar.b1)=[mH,BB]
116 // LOC(localBar.b2)=[mH,BB]
117 // b1 and b2 share the same abstract loc BB
118 // howerver, location BB allows values to be moving within itself
120 localBar.b1++; // value can be moving among the same location
123 public void uniqueReference(){
125 @LOC("methodH") Foo f_1=new Foo();
127 @LOC("methodL") Bar newBar_2;
129 f_1.bar=null; // should assign null here
133 @LATTICE("mL<mM,mM<mH,GLOBALLOC=mH,THISLOC=mL")
134 public void globalField(){
135 @LOC("DELTA(mH,test.testH,Foo.FA)") int value=globalFoo.a; // LOC(globalFoo.a)=[mH,testH,FA]
139 public void globalTopField(){
140 @LOC("methodH") String valueH;
141 valueH=finalValue; // LOC(finalVAlue)=[TOP,testH]
144 public void globalCopy(){
145 // do not allow the below case
146 // it copies something from one calss global variable
147 // to another class global variable
157 @LATTICE("FD<FC,FC<FB,FB<FA")
158 @METHODDEFAULT("fm_L<fm_M1,fm_L<fm_M2,fm_M1<fm_H,fm_M2<fm_H,THISLOC=fm_H")
165 @LOC("FA") static int d;
170 public void doSomething(){
171 b=a; // value flows from [fm_H,FA] to [fm_H,FB]
174 // callee has a constraint that arg1 is higher than arg2
175 public int doSomethingArgs(@LOC("fm_H")int argH,
176 @LOC("fm_M1")int argL){
177 @LOC("fm_L") int value=argL+argH+50;
181 public int doSomethingRtn(){
182 return a+b; // going to return LOC[local.t,field.FB]
185 @LATTICE("L<M,M<H1,M<H2,THISLOC=M")
186 public void unrelatedTwoParams(@LOC("H1")int param1, @LOC("H2") int param2){
187 //since H1 and H2 are not related,
188 //callee doesn't have any ordering constraints on method paramters.
189 @LOC("L") int result=param1+param2;
193 public int callerConstraints(@LOC("H") int param1, @LOC("M") int param2){
195 @LOC("X") int returnValue=100;
199 // return value only has ordering relation with param1, not with param2
200 // but caller expects that all input should have higher
201 // ordering relation than output!
203 // return returnValue;
212 @LATTICE("BC<BB,BB<BA,BB*")
213 @METHODDEFAULT("BARMD_L<BARMD_H,THISLOC=BARMD_H")
219 @LOC("BC") static int d;