Robust/src/Tests/ssJava/flowdown/test.java

   1 @LATTICE("testL<testM,testM<testH")
   2 @METHODDEFAULT("methodL<methodH,methodH<methodT,THISLOC=methodT,GLOBALLOC=methodT")
   3 public class test{
   4
   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";
  12
  13
  14     public static void main (@LOC("methodH") String args[]){
  15         @LOC("methodH") test t=new test();
  16         t.doit();
  17     }
  18
  19     public void doit(){
  20         @LOC("methodH") int localH; // LOC=[local.methodH]
  21         fooM=new Foo(); // LOC=[local.methodT, field.testM]
  22         fooM.doSomething();
  23
  24         // here, callee expects that arg1 is higher than arg2
  25         // so caller should respects callee's constraints
  26         fooM.doSomethingArgs(fieldH,fieldM);
  27
  28         doit2();
  29         doOwnLattice();
  30         doDelta();
  31     }
  32
  33     public void methodInvoke(){
  34         @LOC("methodH") Foo foo=new Foo();
  35
  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);
  40     }
  41
  42     public void doit2(){
  43         @LOC("methodH,test.testL") int localVarL;
  44         // value flows from the field [local.methodH,field.testH]
  45         // to the local variable [local.methodL]
  46         localVarL=fieldH;
  47     }
  48
  49     public void doit3(){
  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)
  53     }
  54
  55     // creating composite location by object references
  56     public void doit4(){
  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]
  61     }
  62
  63     // method has its own local variable lattice
  64     @LATTICE("mL<mH,THISLOC=mH")
  65     public void doOwnLattice(){
  66         @LOC("mL") int varL;
  67         @LOC("mH") int varH;
  68         varL=varH;
  69     }
  70
  71
  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]
  76
  77         @LOC("DELTA(DELTA(mH,test.testH))") int varDeltax2;
  78         // applying double delta to [mH,testH]
  79
  80         varDelta=fieldH; // [mH,testH] -> DELTA[mh,testH]
  81         varDeltax2=varDelta; //DELTA[mh,testH] -> DELTA[DELTA[mh,testH]]
  82
  83         fieldM=varDeltax2; //  DELTA[DELTA[mh,testH]] -> [mH,testM]
  84     }
  85
  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
  90
  91         @LOC("mH") int varH;
  92         @LOC("mSpin") int varSpin;
  93         @LOC("mL") int varL;
  94
  95         varH=10;
  96         while(varSpin>50000){
  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;
 101         }
 102         varL=varSpin;
 103     }
 104
 105     @LATTICE("mL<mH,THISLOC=mL")
 106     public void doSpinField(){
 107         //only last element of the composite location can be the spinning loc
 108
 109         @LOC("mH") int varH;
 110         @LOC("mL") int varL;
 111
 112         @LOC("mH") Bar localBar=new Bar();
 113
 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
 119
 120         localBar.b1++; // value can be moving among the same location
 121     }
 122
 123     public void uniqueReference(){
 124
 125         @LOC("methodH") Foo f_1=new Foo();
 126         f_1.bar=new Bar();
 127         @LOC("methodL") Bar newBar_2;
 128         newBar_2=f_1.bar;
 129         f_1.bar=null; // should assign null here
 130     }
 131
 132
 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]
 136         globalFoo.b=value;
 137     }
 138
 139     public void globalTopField(){
 140         @LOC("methodH") String valueH;
 141         valueH=finalValue; // LOC(finalVAlue)=[TOP,testH]
 142     }
 143
 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
 148
 149         //globalH=Foo.d;
 150     }
 151
 152
 153
 154 }
 155
 156
 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")
 159 class Foo{
 160
 161     @LOC("FA") int a;
 162     @LOC("FB") int b;
 163     @LOC("FC") int c;
 164     @LOC("FC") Bar bar;
 165     @LOC("FA") static int d;
 166
 167     public Foo(){
 168     }
 169
 170     public void doSomething(){
 171         b=a; // value flows from [fm_H,FA] to [fm_H,FB]
 172     }
 173
 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;
 178         return value;
 179     }
 180
 181     public int doSomethingRtn(){
 182         return a+b; // going to return LOC[local.t,field.FB]
 183     }
 184
 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;
 190     }
 191
 192     @LATTICE("M<H,X<H")
 193     public int callerConstraints(@LOC("H") int param1, @LOC("M") int param2){
 194
 195         @LOC("X") int returnValue=100;
 196
 197         if(param1>50){
 198         // ERROR!!!
 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!
 202
 203         // return returnValue;
 204         }
 205
 206
 207         return 0;
 208     }
 209
 210 }
 211
 212 @LATTICE("BC<BB,BB<BA,BB*")
 213 @METHODDEFAULT("BARMD_L<BARMD_H,THISLOC=BARMD_H")
 214 class Bar{
 215     @LOC("BA") int a;
 216     @LOC("BB") int b2;
 217     @LOC("BB") int b1;
 218     @LOC("BC") int c;
 219     @LOC("BC") static int d;
 220 }
 221