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 doit2(){
  34         @LOC("methodH,testL") int localVarL;
  35         // value flows from the field [local.methodH,field.testH]
  36         // to the local variable [local.methodL]
  37         localVarL=fieldH;
  38     }
  39
  40     public void doit3(){
  41         @LOC("methodT,testL")int localVar=fooM.a+fooM.b;
  42         // GLB(fooM.a,fooM.b)=LOC[methodT,testM,FB]
  43         // LOC[lovalVar]=[methodT,testL] < GLB(fooM.a,fooM.b)
  44     }
  45
  46     // creating composite location by object references
  47     public void doit4(){
  48         @LOC("methodT,testM,FC,BB") int localVar=fooM.bar.a;
  49         //LOC(fooM.bar.a)=[methodT,testM,FC,BA]
  50         //localVar can flow into lower location of fooM.bar.a
  51         fooM.bar.c=localVar; //[methodT,testM,FC,BB] < [methodT,testM,FC,BA]
  52     }
  53
  54     // method has its own local variable lattice
  55     @LATTICE("mL<mH,THISLOC=mH")
  56     public void doOwnLattice(){
  57         @LOC("mL") int varL;
  58         @LOC("mH") int varH;
  59         varL=varH;
  60     }
  61
  62
  63     @LATTICE("mL<mH,THISLOC=mH")
  64     public void doDelta(){
  65         @LOC("DELTA(mH,testH)") int varDelta;
  66         // LOC(varDelta) is slightly lower than [mH, testH]
  67
  68         @LOC("DELTA(DELTA(mH,testH))") int varDeltax2;
  69         // applying double delta to [mH,testH]
  70
  71         varDelta=fieldH; // [mH,testH] -> DELTA[mh,testH]
  72         varDeltax2=varDelta; //DELTA[mh,testH] -> DELTA[DELTA[mh,testH]]
  73
  74         fieldM=varDeltax2; //  DELTA[DELTA[mh,testH]] -> [mH,testM]
  75     }
  76
  77     @LATTICE("mL<mSpin,mSpin<mH,mSpin*")
  78     public void doSpinLoc(){
  79         // if loc is defined with the suffix *,
  80         //value can be flowing around the same location
  81
  82         @LOC("mH") int varH;
  83         @LOC("mSpin") int varSpin;
  84         @LOC("mL") int varL;
  85
  86         varH=10;
  87         while(varSpin>50000){
  88             // value can be flowing back to the varSpin
  89             // since 'varSpin' is location allowing value to move within
  90             // the same abstract location
  91             varSpin=varSpin+varH;
  92         }
  93         varL=varSpin;
  94     }
  95
  96     @LATTICE("mL<mH,THISLOC=mL")
  97     public void doSpinField(){
  98         //only last element of the composite location can be the spinning loc
  99
 100         @LOC("mH") int varH;
 101         @LOC("mL") int varL;
 102
 103         @LOC("mH") Bar localBar=new Bar();
 104
 105         localBar.b2=localBar.b1;
 106         // LOC(localBar.b1)=[mH,BB]
 107         // LOC(localBar.b2)=[mH,BB]
 108         // b1 and b2 share the same abstract loc BB
 109         // howerver, location BB allows values to be moving within itself
 110
 111         localBar.b1++; // value can be moving among the same location
 112     }
 113
 114     public void uniqueReference(){
 115
 116         @LOC("methodH") Foo f_1=new Foo();
 117         f_1.bar=new Bar();
 118         @LOC("methodL") Bar newBar_2;
 119         newBar_2=f_1.bar;
 120         f_1.bar=null; // should assign null here
 121     }
 122
 123
 124     @LATTICE("mL<mM,mM<mH,GLOBALLOC=mH,THISLOC=mL")
 125     public void globalField(){
 126         @LOC("DELTA(mH,testH,FA)") int value=globalFoo.a; // LOC(globalFoo.a)=[mH,testH,FA]
 127         globalFoo.b=value;
 128     }
 129
 130     public void globalTopField(){
 131         @LOC("methodH") String valueH;
 132         valueH=finalValue; // LOC(finalVAlue)=[TOP,testH]
 133     }
 134
 135     public void globalCopy(){
 136         // do not allow the below case
 137         // it copies something from one calss global variable
 138         // to another class global variable
 139
 140         //globalH=Foo.d;
 141     }
 142
 143 }
 144
 145
 146 @LATTICE("FD<FC,FC<FB,FB<FA")
 147 @METHODDEFAULT("fm_L<fm_M1,fm_L<fm_M2,fm_M1<fm_H,fm_M2<fm_H,THISLOC=fm_H")
 148 class Foo{
 149
 150     @LOC("FA") int a;
 151     @LOC("FB") int b;
 152     @LOC("FC") int c;
 153     @LOC("FC") Bar bar;
 154     @LOC("FA") static int d;
 155
 156     public Foo(){
 157     }
 158
 159     public void doSomething(){
 160         b=a; // value flows from [fm_H,FA] to [fm_H,FB]
 161     }
 162
 163     // callee has a constraint that arg1 is higher than arg2
 164     public int doSomethingArgs(@LOC("fm_H")int argH,
 165                                @LOC("fm_M1")int argL){
 166         argL=argH+50;
 167         return argL;
 168     }
 169
 170     public int doSomethingRtn(){
 171         return a+b; // going to return LOC[local.t,field.FB]
 172     }
 173
 174 }
 175
 176 @LATTICE("BC<BB,BB<BA,BB*")
 177 @METHODDEFAULT("BARMD_L<BARMD_H,THISLOC=BARMD_H")
 178 class Bar{
 179     @LOC("BA") int a;
 180     @LOC("BB") int b2;
 181     @LOC("BB") int b1;
 182     @LOC("BC") int c;
 183     @LOC("BC") static int d;
 184
 185
 186 }