/* For inclusion by a Tvp program

Requires "Fields,VarAll" to be defined

Depends on ID_PRED, ANCESTOR

Defines 

InstrumField1: is[field, mode](v) (shared), c[field,mode](v) (cyclicity), 
InstrumField2: Star[field,mode]
InstrumFieldVar1: r[field,mode,var] (reachability), (a[field,mode,var]) (coreachability/ancestor)
InstrumFieldVar2: 
InstrumMode1: 
InstrumMode2: 
InstrumModeVar1: 
InstrumModeVar2: 
CrossInstrum1:
CrossInstrum2:
CrossInstrumField1: (id_pred[field,mode1,mode2]), id_succ[field,mode1,mode2]
CrossInstrumField2:
*/

/* Explanations

- InstrumField: depends only on a "field" predicate

- InstrumFieldVar: depends only on a field predicate
  and a local variable predicate

- InstrumMode: depends only on core predicates giving heap information

- InstrumModeVar: depends only on core predicates giving heap information and
  one local variable predicate

- CrossInstrum: any cross-instrumentation predicate

- CrossInstrumField: cross-instrumentation predicate depending only on a field
  predicate.
*/

// **********************************************************************
// **********************************************************************
// SETS and PREDICATE DECLARATIONS
// **********************************************************************
// **********************************************************************

%s Mode {inp,out,ext}
%s InstrumField1 {is,c}
%s InstrumField2 {Star}
%s InstrumFieldVar1 {r}
#ifdef ANCESTOR
%s InstrumFieldVar1 InstrumFieldVar1 + { a }
#endif
%s InstrumFieldVar2 {}
%s InstrumMode1 {}
%s InstrumMode2 {}
%s InstrumModeVar1 {}
%s InstrumModeVar2 {}

%s CrossInstrum1 {}
%s CrossInstrum2 {}
%s CrossInstrumField1 { id_succ }
#ifdef ID_PRED
%s CrossInstrumField1 CrossInstrumField1 + { id_pred }
#endif

%s CrossInstrumField2 {}

// ======================================================================
// Program variables
// ======================================================================

%s VarAllFPR VarAll+FP+FR

foreach (z in VarAllFPR){
%p z(v_1) unique pointer
}


// ======================================================================
// Fields
// ======================================================================

foreach (b in Bools){
  foreach (m in Mode){
    %p b[m](v_1)
  }
}

foreach (f in Fields){
  foreach (m in Mode){
    %p f[m](v_1, v_2) function
  }
}

// ======================================================================
// Instrumentation
// ======================================================================

foreach (m in Mode){
  foreach (f in Fields){
    // Transitive closure
    %i Star[f,m](v_1,v_2) = f[m]*(v_1, v_2) transitive reflexive nonabs

    // IsShared
    %i is[f,m](v) = E(v_1, v_2) ( v_1 != v_2 & f[m](v_1, v) & f[m](v_2, v)) abs

    // Cyclicity
    %i c[f,m](v) = E(v_1) (f[m](v_1, v) & Star[f,m](v, v_1)) abs
    
    // r[f,m,z](v) : reachability of nodes from variables via f
    foreach (z in VarAllFPR) {
      %i r[f,m,z](v) = E(v_1) (z(v_1) & Star[f,m](v_1,v)) abs
    }
    // a[f,m,z](v) : coreachability of nodes from variables via f
#ifdef ANCESTOR
    foreach (z in VarAllFPR) {
      %i a[f,m,z](v) = E(v_1) (z(v_1) & Star[f,m](v,v_1)) abs
    }
#endif
  }
}

// ======================================================================
// Rules
// ======================================================================

// Trivial consequences of definitions of f,r,Star
foreach (m in Mode){
  foreach (f in Fields) {
    %r E(v_2) (Star[f,m](v_1, v_2) & Star[f,m](v_2,v_3)) ==> Star[f,m](v_1,v_3)
    %r !Star[f,m](v_1,v_2) ==> !f[m](v_1,v_2)

    %r f[m](v_1,v_2) ==> Star[f,m](v_1,v_2)

    foreach (z in VarAllFPR){
      %r z(v_1) & r[f,m,z](v_2) ==> Star[f,m](v_1,v_2)
      %r z(v_1) & Star[f,m](v_1,v_2) ==> r[f,m,z](v_2)
      %r z(v_1) & !r[f,m,z](v_2) ==> !Star[f,m](v_1,v_2)
      %r z(v_1) & !Star[f,m](v_1,v_2) ==> !r[f,m,z](v_2)
      %r r[f,m,z](v_1) & !r[f,m,z](v_2) ==> !Star[f,m](v_1,v_2) 
      %r r[f,m,z](v_1) & r[f,m,z](v_2) & !Star[f,m](v_1,v_2) ==> Star[f,m](v_2,v_1) 
#ifdef ANCESTOR
      %r z(v_1) & a[f,m,z](v_2) ==> Star[f,m](v_2,v_1)
      %r z(v_1) & Star[f,m](v_2,v_1) ==> a[f,m,z](v_2)
      %r z(v_1) & !a[f,m,z](v_2) ==> !Star[f,m](v_2,v_1)
      %r z(v_1) & !Star[f,m](v_2,v_1) ==> !a[f,m,z](v_2)
      %r a[f,m,z](v_1) & !a[f,m,z](v_2) ==> !Star[f,m](v_2,v_1) 
#endif
    }  
  }
}

// Transitivity of Star
foreach (m in Mode){
  foreach (f in Fields) {
    %r (E(v) Star[f,m](v, v_1) & !Star[f,m](v, v_2)) ==> !Star[f,m](v_1, v_2)
    %r (E(v) Star[f,m](v_1, v) & Star[f,m](v, v_2)) ==> Star[f,m](v_1, v_2)
  }
}

// Acyclicity of downStar
foreach (m in Mode){
  foreach (f in Fields) {
    %r Star[f,m](v_1, v_2) & !c[f,m](v_1) ==> !f[m](v_2, v_1)
  }
}

// reachability and coreachability
#ifdef ANCESTOR
foreach (m in Mode){
  foreach (f in Fields) {
    foreach (z in VarAllFPR){
      %r !z(v) & r[f,m,z](v) & a[f,m,z](v) ==> c[f,m](v)
      %r !z(v) & r[f,m,z](v) & !c[f,m](v) ==> !a[f,m,z](v)
      %r !z(v) & a[f,m,z](v) & !c[f,m](v) ==> !r[f,m,z](v)
    }
  }
}
#endif

// ======================================================================
// Cross instrumentation predicates
// ======================================================================

foreach (f in Fields){
  foreach (m1 in Mode){
    foreach (m2 in Mode - { m1 }){

#ifdef ID_PRED
      %i id_pred[f,m1,m2](v) = A(v_1) ( f[m1](v_1,v) -> f[m2](v_1,v) ) abs
      %r !f[m2](v_1,v_2) & id_pred[f,m1,m2](v_2) ==> !f[m1](v_1,v_2)
#endif

      %i id_succ[f,m1,m2](v) = A(v_1) ( f[m1](v,v_1) -> f[m2](v,v_1) ) abs
//    %r f[m1](v_1,v_2) & id_succ[f,m1,m2](v_1) ==> f[m2](v_1,v_2)
//    %r !f[m2](v_1,v_2) & id_succ[f,m1,m2](v_1) ==> !f[m1](v_1,v_2)
    }
  }
}

// Rules linking cross predicates
foreach (f in Fields){
foreach (m1 in Mode){
  foreach (m2 in Mode - {m1}){
    foreach (m3 in Mode - {m1,m2}){
#ifdef ID_PRED
      %r id_pred[f,m1,m2](v) & id_pred[f,m2,m3](v) ==> id_pred[f,m1,m3](v)
#endif
      %r id_succ[f,m1,m2](v) & id_succ[f,m2,m3](v) ==> id_succ[f,m1,m3](v)
    }
  }
}
}

// ======================================================================
// Cross instrumentation rules
// ======================================================================

// Important: linking reachability in different modes

foreach (m1 in Mode){
  foreach (m2 in Mode-{m1}){
    foreach(f in Fields){
      foreach (zz in VarAllFPR){
%r r[f,m1,zz](v) & (A(v_1) (r[f,m1,zz](v) -> id_succ[f,m1,m2](v_1))) 
   ==> r[f,m2,zz](v)
#ifdef ANCESTOR
%r a[f,m1,zz](v) & (A(v_1) ((a[f,m1,zz](v) & !zz(v)) -> id_succ[f,m1,m2](v_1)))
   ==> a[f,m2,zz](v)
#endif
      }
    }
  }
}