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

   1 @LATTICE("testL<testM,testM<testH")
   2 @METHODDEFAULT("methodL<methodH,methodH<methodT,THISLOC=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
  10     public static void main (@LOC("methodH") String args[]){
  11         @LOC("methodH") test t=new test();
  12         t.doit();
  13     }
  14
  15     public void doit(){
  16         @LOC("methodH") int localH; // LOC=[local.methodH]
  17         fooM=new Foo(); // LOC=[local.methodT, field.testM]
  18         fooM.doSomething();
  19
  20         // here, callee expects that arg1 is higher than arg2
  21         // so caller should respects callee's constraints
  22         fooM.doSomethingArgs(fieldH,fieldM);
  23
  24         doit2();
  25         doOwnLattice();
  26         doDelta();
  27     }
  28
  29     public void doit2(){
  30         @LOC("methodH,testL") int localVarL;
  31         // value flows from the field [local.methodH,field.testH]
  32         // to the local variable [local.methodL]
  33         localVarL=fieldH;
  34     }
  35
  36     public void doit3(){
  37         @LOC("methodT,testL")int localVar=fooM.a+fooM.b;
  38         // GLB(fooM.a,fooM.b)=LOC[methodT,testM,FB]
  39         // LOC[lovalVar]=[methodT,testL] < GLB(fooM.a,fooM.b)
  40     }
  41
  42     // creating composite location by object references
  43     public void doit4(){
  44         @LOC("methodT,testM,FC,BB") int localVar=fooM.bar.a;
  45         //LOC(fooM.bar.a)=[methodT,testM,FC,BA]
  46         //localVar can flow into lower location of fooM.bar.a
  47         fooM.bar.c=localVar; //[methodT,testM,FC,BB] < [methodT,testM,FC,BA]
  48     }
  49
  50     // method has its own local variable lattice
  51     @LATTICE("mL<mH,THISLOC=mH")
  52     public void doOwnLattice(){
  53         @LOC("mL") int varL;
  54         @LOC("mH") int varH;
  55         varL=varH;
  56     }
  57
  58
  59     @LATTICE("mL<mH,THISLOC=mH")
  60     public void doDelta(){
  61         @LOC("DELTA(mH,testH)") int varDelta;
  62         // LOC(varDelta) is slightly lower than [mH, testH]
  63
  64         @LOC("DELTA(DELTA(mH,testH))") int varDeltax2;
  65         // applying double delta to [mH,testH]
  66
  67         varDelta=fieldH; // [mH,testH] -> DELTA[mh,testH]
  68         varDeltax2=varDelta; //DELTA[mh,testH] -> DELTA[DELTA[mh,testH]]
  69
  70         fieldM=varDeltax2; //  DELTA[DELTA[mh,testH]] -> [mH,testM]
  71     }
  72
  73     @LATTICE("mL<mSpin,mSpin<mH,mSpin*")
  74     public void doSpinLoc(){
  75         // if loc is defined with the suffix *,
  76         //value can be flowing around the same location
  77
  78         @LOC("mH") int varH;
  79         @LOC("mSpin") int varSpin;
  80         @LOC("mL") int varL;
  81
  82         varH=10;
  83         while(varSpin>50000){
  84             // value can be flowing back to the varSpin
  85             // since 'varSpin' is location allowing value to move within
  86             // the same abstract location
  87             varSpin=varSpin+varH;
  88         }
  89         varL=varSpin;
  90     }
  91
  92     @LATTICE("mL<mH,THISLOC=mL")
  93     public void doSpinField(){
  94
  95         @LOC("mH") int varH;
  96         @LOC("mL") int varL;
  97
  98         @LOC("mH") Bar localBar=new Bar();
  99
 100         localBar.b2=localBar.b1;
 101         // LOC(localBar.b1)=[mH,BB]
 102         // LOC(localBar.b2)=[mH,BB]
 103         // b1 and b2 share the same abstract loc BB
 104         // howerver, location BB allows values to be moving within itself
 105
 106         localBar.b1++; // value can be moving among the same location
 107     }
 108 }
 109
 110
 111 @LATTICE("FC<FB,FB<FA")
 112 @METHODDEFAULT("fm_L<fm_M1,fm_L<fm_M2,fm_M1<fm_H,fm_M2<fm_H,THISLOC=fm_H")
 113 class Foo{
 114
 115     @LOC("FA") int a;
 116     @LOC("FB") int b;
 117     @LOC("FC") int c;
 118     @LOC("FC") Bar bar;
 119
 120     public Foo(){
 121     }
 122
 123     public void doSomething(){
 124         b=a; // value flows from [fm_H,FA] to [fm_H,FB]
 125     }
 126
 127     // callee has a constraint that arg1 is higher than arg2
 128     public int doSomethingArgs(@LOC("fm_H")int argH,
 129                                @LOC("fm_M1")int argL){
 130         argL=argH+50;
 131         return argL;
 132     }
 133
 134     public int doSomethingRtn(){
 135         return a+b; // going to return LOC[local.t,field.FB]
 136     }
 137
 138 }
 139
 140 @LATTICE("BC<BB,BB<BA,BB*")
 141 class Bar{
 142     @LOC("BA") int a;
 143     @LOC("BB") int b2;
 144     @LOC("BB") int b1;
 145     @LOC("BC") int c;
 146
 147 }