JavaMOP Properties

From FSL
Jump to: navigation, search

Back to JavaMOPCFG

Contents

HashMap

package mop;
import java.util.*;

/*@
sync
partial
scope = global
logic = CFG
HashMap (HashMap t, Object o){
  [int hashcode=0;]
  event put <t, o> : end(call(* t.put(o, Object))) && !within(java..*) && !within(org.apache.commons..*) 
    && !within   (com.sun..*) && !within(sun..*) && !within(sunw..*) && !within(dacapo..*) 
    && !within(tests..*) {hashcode = o.hashCode();};
  event remove <t, o>: end(call(* t.remove(o))) && !within(java..*) && !within(org.apache.commons..*) 
    && !within(com.sun..*) && !within(sun..*) && !within(sunw..*) && !within(dacapo..*) && !within(tests..*);
  event use <t, o> : begin(call(* t.contai*(o))) && !within(java..*) && !within(org.apache.commons..*) 
    && !within(com.sun..*) && !within(sun..*) && !within(sunw..*) && !within(dacapo..*) && !within(tests..*);
  start symbol : S
  productions : S -> put use

}
Validation handler {
if (@MONITOR.hashcode != o.hashCode())
        System.out.println("HashCode changed for Object " + o + " while being in a Hashtable.");
}
@*/

HasNext

package mop;

/*@
sync
partial
scope = global
logic = CFG
HasNext(Iterator i)
{
  event hasnext <i> : end(exec(* i.hasNext())) && !within(java..*) && !within(org.apache.commons..*) 
    && !within(com.sun..*) && !within(sun..*) && !within(sunw..*) && !within(dacapo..*) && !within(tests..*);
  event next <i> : begin(exec(* i.next())) && !within(java..*) && !within(org.apache.commons..*) 
    && !within(com.sun..*) && !within(sun..*) && !within(sunw..*) && !within(dacapo..*) && !within(tests..*);
  start symbol : S
  productions : S -> next next 
}
Validation handler{
      System.err.println("! hasNext() has not been called before calling next() for an iterator");
      //Thread.dumpStack();
}
@*/

SafeIterator

package mop;

import java.util.*;

/*@ 
sync
partial
scope = global
logic = CFG
SafeIterator (Collection+ c, Iterator+ i) {
  event create<i, c> : end(call(Iterator c.iterator())) with (i) && !within(dacapo..*) && !within(tests..*) 
    && !within(java..*) && !within(org.apache.commons..*) && !within(com.sun..*) && !within(sun..*) 
    && !within(sunw..*);
  event updatesource<c> : end(call(* c.remove*(..))) && !within(dacapo..*) && !within(tests..*) 
    && !within(java..*) && !within(org.apache.commons..*) && !within(com.sun..*) && !within(sun..*) 
    && !within(sunw..*) \/ end(call(* c.add*(..))) && !within(dacapo..*) && !within(tests..*) 
    && !within(java..*) && !within(org.apache.commons..*) && !within(com.sun..*) && !within(sun..*) 
    && !within(sunw..*);
  event next<i> : begin(call(Object i.next() )) && !within(dacapo..*) && !within(tests..*) 
    && !within(java..*) && !within(org.apache.commons..*) && !within(com.sun..*) && !within(sun..*) 
    && !within(sunw..*);
  start symbol : S
  productions : S -> create NextStar updatesource UpdateStar next,
        NextStar -> NextStar next | epsilon,
        UpdateStar -> UpdateStar updatesource | epsilon
}
validation handler {
   System.out.println("the collection is changed during iterating!");
}
@*/

ImprovedLeakingSync

package mop;

import java.util.*;

/*@
sync
partial
scope = global
logic = CFG
LeakingSyncCFG (Collection o, Collection syncO)
{
   event create<o, syncO> : end(call(* Collections.synchronizedCollection(o))) with (syncO) 
     && !within(dacapo..*) && !within(tests..*) && !within(java..*) && !within(org.apache.commons..*) 
     && !within(com.sun..*) && !within(sun..*) && !within(sunw..*);
   event access<o> : begin(call(* o.*(..))) && !within(dacapo..*) && !within(tests..*) && !within(java..*) 
     && !within(org.apache.commons..*) && !within(com.sun..*) && !within(sun..*) && !within(sunw..*);
   event syncBegin<syncO> : begin(exec(* syncO.*(..))) && !within(dacapo..*) && !within(tests..*) 
     && !within(java..*) && !within(org.apache.commons..*) && !within(com.sun..*) && !within(sun..*) && !within(sunw..*);
   event syncEnd<syncO> : end(exec(* syncO.*(..))) && !within(dacapo..*) && !within(tests..*) 
     && !within(java..*) && !within(org.apache.commons..*) && !within(com.sun..*) && !within(sun..*) && !within(sunw..*);
   start symbol : S
   productions : S -> create SyncUseStar access,
         SyncUseStar -> SyncUseStar SyncUse | epsilon,
         SyncUse -> syncBegin SyncUse2 syncEnd,
         SyncUse2 -> SyncUse2 SyncUse | access | epsilon
}
Validation handler {
   System.out.println("leaked sync!");
}
@*/

SafeFileInputStream

  • In this example, we used static analysis both on MOP and Tracematches.

To apply static analysis on MOP, use this patch

package mop;

import java.io.*;

/*@
sync
partial
scope = global
logic = CFG
SafeFileInputStreamCFG (FileInputStream fi)
{
  event sysBegin :  begin(call(* *.*(..)))&& !within (dacapo..* ) && !within (tests..* ) 
    && !within (java..*) && !within (org.apache.commons..*) && !within (com.sun..*) 
    && !within (sun..*) && !within (sunw..*);
  event sysEnd : end(call(* *.*(..))) && !within(dacapo..*) && !within(tests..*) 
    && !within (java..*) && !within (org.apache.commons..*) && !within (com.sun..*) 
    && !within (sun..*) && !within (sunw..*);
  event create<fi> : end(call(FileInputStream.new(..))) with (fi) && !within(dacapo..*) 
    && !within(tests..*) && !within(java..*) && !within(org.apache.commons..*) && !within(com.sun..*) 
    && !within(sun..*) && !within(sunw..*);
  event close<fi> : end(call(* fi.close())) && !within(dacapo..*) && !within(tests..*) 
    && !within(java..*) && !within(org.apache.commons..*) && !within(com.sun..*) && !within(sun..*) 
    && !within(sunw..*);
  start symbol : S
  productions  : S -> create Pairs sysEnd,
                 Pairs -> Pairs sysBegin create sysEnd | Pairs sysBegin Pairs sysEnd | epsilon
}

Validation handler{
System.err.println("unmatched open/close");
//Thread.dumpStack();
}
@*/

SafeFileWriter

package mop;

import java.io.*;

/*@
sync
partial
scope = global
logic = CFG
SafeFileWriter(FileWriter f){
  event open<f> : end(call(FileWriter.new(..))) with (f);
  event write<f> : end(call(* f.write(..)));
  event close<f> : end(call(* f.close(..)));
  start symbol : S
  productions : S -> open SafeWrite close write,
        SafeWrite ->  SafeWrite S | SafeWrite write | epsilon
}
validation handler{ 
  System.out.println("write after close");
}
@*/
Personal tools
Namespaces

Variants
Actions
Navigation