/* A Tvp program for reverse

*/

#define COMPLETE


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

// ====================================================================== 
// Program variables and fields
// ====================================================================== 

%s DeleteVar	{h,c,t,l}

%s MainVar	{ list,res,cell }

%s VarAll	DeleteVar + MainVar

%s Fields { n }
%s Bools { }

%s FP { fp1 }
%s FR { fr1,fr2 }

// ====================================================================== 
// Standard predicates
// ====================================================================== 

#include "predicate.tvp" 

// ======================================================================
// specific instrumentation predicates
// ======================================================================

/* These are necessary to avoid the "relational pattern" to be blurred. */

%s InstrumFieldVar1 InstrumFieldVar1 + { succ,pred }

foreach (m in Mode){
  foreach (f in Fields){
    // Definitions
    foreach (z in VarAllFPR - { cell,c,fr2} ){
      %i succ[f,m,z](v) = E(v_1) z(v_1) & f[m](v_1,v) nonabs unique
      %i pred[f,m,z](v) = E(v_1) z(v_1) & f[m](v,v_1) nonabs
    }
    foreach (z in { cell,c,fr2}){
      %i succ[f,m,z](v) = E(v_1) z(v_1) & f[m](v_1,v) abs unique
      %i pred[f,m,z](v) = E(v_1) z(v_1) & f[m](v,v_1) abs
    }
  }
}

%%

// **********************************************************************
// FUNCTION DEFINITIONS
// **********************************************************************

#include "function.tvp" 

// ======================================================================
// Standard Blur at entry (what is not reachable at entry is abstracted)
// ======================================================================

%function FocusPattern[](X)
    %t "FocusPattern"
{
    begin
      focus(X, { c(v), pred[n,inp,c](v), succ[n,inp,c](v), r[n,inp,c](v) });
      X
    end
}

// ======================================================================
// Standard Blur at entry (what is not reachable at entry is abstracted)
// ======================================================================

%function BlurEntry[](X)
    %t "BlurEntry"
{
  begin
    focus(X, { r[n,out,h](v) });
    let Y = transform(X,
	update:{
sm(v) = ( (r[n,out,h](v)) ? sm(v) : 1/2 )
// Cross-instrumentation
foreach(m in {inp,out}){
  foreach (f in Fields){
    foreach(p in CrossInstrumField1){
      p[f,ext,m](v) = 1/2
      p[f,m,ext](v) = 1/2
    }
    foreach(p in CrossInstrumField2){
      p[f,ext,m](v_1,v_2) = 1/2
      p[f,m,ext](v_1,v_2) = 1/2
    }
  }
  foreach(p in CrossInstrum1){
    p[ext,m](v) = 1/2
    p[m,ext](v) = 1/2
  }
  foreach(p in CrossInstrum2){
    p[ext,m](v_1,v_2) = 1/2
    p[m,ext](v_1,v_2) = 1/2
  }
}
})
    in begin
      blur(Y);
      coerce(Y);
      Y
    end
  end
}

// ======================================================================
// Standard Blur at the end (what is not reachable at entry is abstracted)
// ======================================================================

%function BlurSummary[](X)
    %t "BlurSummary"
{
  begin
    focus(X, { r[n,out,fp1](v) });
    let Y = transform(X,
	update:{
sm(v) = ( (r[n,out,fp1](v)) ? sm(v) : 1/2 )
// Cross-instrumentation
foreach(m in {out,ext}){
  foreach (f in Fields){
    foreach(p in CrossInstrumField1){
      p[f,inp,m](v) = 1/2
      p[f,m,inp](v) = 1/2
    }
    foreach(p in CrossInstrumField2){
      p[f,inp,m](v_1,v_2) = 1/2
      p[f,m,inp](v_1,v_2) = 1/2
    }
  }
  foreach(p in CrossInstrum1){
    p[inp,m](v) = 1/2
    p[m,inp](v) = 1/2
  }
  foreach(p in CrossInstrum2){
    p[inp,m](v_1,v_2) = 1/2
    p[m,inp](v_1,v_2) = 1/2
  }
}
})
    in begin
      blur(Y);
      coerce(Y);
      Y
    end
  end
}

// ======================================================================
// Special return operation, because additional focusing
// ======================================================================

/* This due to the fact that one remove a cell in a list */

%function myret_2_1[ret1, ret2, name, act1](Xcaller,Xcallee)
     %t "MyRet_2_1 (" + ret1 + ", " + ret2 +") := " + name + "(" + act1 + ")"
{
  begin
    // Conversion to constraints
    toconstraints(Xcallee);
    // We put [ext] fields to 1/2 and equate fp1 to act1 in Xcaller
    let Xcaller = transform(Xcaller,
			 update: {
// We put [ext] fields to 1/2
 foreach (f in Bools){ f[ext](v) = 1/2 }
 foreach (f in Fields){ f[ext](v_1,v_2) = 1/2 }
// We make fr1 non determinated
fr1(v) = 1/2
fr2(v) = 1/2
// We equate fp1 to act1 in Xcaller
fp1(v) = act1(v)
foreach (f in Fields){
  foreach (p in InstrumFieldVar1){ 
    p[f,out,fp1](v) = p[f,out,act1](v) 
  }
  foreach (p in InstrumFieldVar2){ 
    p[f,out,fp1](v_1,v_2) = p[f,out,act1](v_1,v_2) 
  }
}
foreach (p in InstrumModeVar1){ 
  p[out,fp1](v) = p[out,act1](v) 
}
foreach (p in InstrumModeVar2){ 
  p[out,fp1](v_1,v_2) = p[out,act1](v_1,v_2) 
}
// Input, Output left identical
foreach (m in {inp,out}){
  // Arity 1&2
  foreach (f in Fields){
    foreach (p in InstrumField1){ p[f,m](v) = p[f,m](v) }
    foreach (p in InstrumField2){ p[f,m](v_1,v_2) = p[f,m](v_1,v_2) }
    foreach (zz in VarAllFPR - {fp1,fr1,fr2}){
      foreach (p in InstrumFieldVar1){ p[f,m,zz](v) = p[f,m,zz](v) }
      foreach (p in InstrumFieldVar2){ p[f,m,zz](v_1,v_2) = p[f,m,zz](v_1,v_2) }
    }
  }
  foreach (p in InstrumMode1){ p[m](v) = p[m](v) }
  foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) }
  foreach (zz in VarAllFPR - {fp1,fr1,fr2}){
    foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) }
    foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) }
  }
}
// Cross Instrumentation left identical
foreach (m1 in Mode-{ext}){
  foreach (m2 in Mode-{m1,ext}){
    foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) }
    foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) }
    foreach (f in Fields){
      foreach (p in CrossInstrumField1){ p[f,m1,m2](v) = p[f,m1,m2](v) }
      foreach (p in CrossInstrumField2){ p[f,m1,m2](v_1,v_2) = p[f,m1,m2](v_1,v_2) }
    }
  }
}
})
    in begin
    push(Xcaller,Xcallee);    // We add them to Xcaller
    focus(Xcaller, { fr1(v), fr2(v), succ[n,out,fr2](v), pred[n,out,fr2](v), r[n,out,fr2](v), r[n,inp,fr2](v) }); // We make f1(v) appear in Xmain
    // Coerce is applied after focus (we suppose the right option is turned on)
    pop(Xcaller);       // We go back to the standard set of constraints
    /* We do several things the same time here. Semantically,
       1. we perform the assignement ret1 := fr1
       2. we get rid of predicates related to the callee (fp1 and fr1, and related instrumentation)
       3. we eliminate predicates with 'out' mode
       4. we perform the shift 'ext' -> 'out'
       Practically, we do it in one step. In the same time
       - we get rid of predicates related to the callee
       - we eliminate predicates with 'ext' mode
       - we assign 'out' to 'ext'
       The assignement is performed together with the shift
    */
    let Y = transform(Xcaller,
		    update:{
ret1(v) = fr1(v)
ret2(v) = fr2(v)
fp1(v) = 1/2
fr1(v) = 1/2
fr2(v) = 1/2
foreach (f in Bools){
  f[out](v) = f[ext](v)
  f[ext](v) = 1/2
}
foreach (f in Fields){
  f[out](v_1,v_2) = f[ext](v_1,v_2)
  f[ext](v_1,v_2) = 1/2
}
foreach (f in Fields){
  foreach (p in InstrumField1){
    p[f,inp](v) = p[f,inp](v)
    p[f,out](v) = p[f,ext](v)
    p[f,ext](v) = 1/2
  }
  foreach (p in InstrumField2){
    p[f,inp](v_1,v_2) = p[f,inp](v_1,v_2)
    p[f,out](v_1,v_2) = p[f,ext](v_1,v_2)
    p[f,ext](v_1,v_2) = 1/2
  }
  foreach (p in InstrumFieldVar1){
    foreach (zz in FP+FR){
      foreach (m in Mode){ 
        p[f,m,zz](v) = 1/2 
      }
    }
    p[f,inp,ret1](v) = p[f,inp,fr1](v)
    p[f,out,ret1](v) = p[f,ext,fr1](v)
    p[f,ext,ret1](v) = 1/2
    p[f,inp,ret2](v) = p[f,inp,fr2](v)
    p[f,out,ret2](v) = p[f,ext,fr2](v)
    p[f,ext,ret2](v) = 1/2
    foreach (zz in VarAll-{ret1,ret2}){
      p[f,inp,zz](v) = p[f,inp,zz](v)
      p[f,out,zz](v) = p[f,ext,zz](v)
      p[f,ext,zz](v) = 1/2
    }
  }
  foreach (p in InstrumFieldVar2){
    foreach (zz in FP+FR){
      foreach (m in Mode){ 
        p[f,m,zz](v_1,v_2) = 1/2 
      }
    }
    p[f,inp,ret1](v_1,v_2) = p[f,inp,fr1](v_1,v_2)
    p[f,out,ret1](v_1,v_2) = p[f,ext,fr1](v_1,v_2)
    p[f,ext,ret1](v_1,v_2) = 1/2
    p[f,inp,ret2](v_1,v_2) = p[f,inp,fr2](v_1,v_2)
    p[f,out,ret2](v_1,v_2) = p[f,ext,fr2](v_1,v_2)
    p[f,ext,ret2](v_1,v_2) = 1/2
    foreach (zz in VarAll-{ret1,ret2}){
      p[f,inp,zz](v_1,v_2) = p[f,inp,zz](v_1,v_2)
      p[f,out,zz](v_1,v_2) = p[f,ext,zz](v_1,v_2)
      p[f,ext,zz](v_1,v_2) = 1/2
    }
  }
}
foreach (p in InstrumMode1){
  p[inp](v) = p[inp](v)
  p[out](v) = p[ext](v)
  p[ext](v) = 1/2
}
foreach (p in InstrumMode2){
  p[inp](v_1,v_2) = p[inp](v_1,v_2)
  p[out](v_1,v_2) = p[ext](v_1,v_2)
  p[ext](v_1,v_2) = 1/2
}
foreach (p in InstrumModeVar1){
  foreach (zz in FP+FR){
    foreach (m in Mode){ 
      p[m,zz](v) = 1/2      
    }
  }
  p[inp,ret1](v) = p[inp,fr1](v)
  p[out,ret1](v) = p[ext,fr1](v)
  p[ext,ret1](v) = 1/2
  p[inp,ret2](v) = p[inp,fr2](v)
  p[out,ret2](v) = p[ext,fr2](v)
  p[ext,ret2](v) = 1/2
  foreach (zz in VarAll-{ret1,ret2}){
    p[inp,zz](v) = p[inp,zz](v)
    p[out,zz](v) = p[ext,zz](v)
    p[ext,zz](v) = 1/2
  }
}
foreach (p in InstrumModeVar2){
  foreach (zz in FP+FR){
    foreach (m in Mode){ 
      p[m,zz](v_1,v_2) = 1/2      
    }
  }
  p[inp,ret1](v_1,v_2) = p[inp,fr1](v_1,v_2)
  p[out,ret1](v_1,v_2) = p[ext,fr1](v_1,v_2)
  p[ext,ret1](v_1,v_2) = 1/2
  p[inp,ret2](v_1,v_2) = p[inp,fr2](v_1,v_2)
  p[out,ret2](v_1,v_2) = p[ext,fr2](v_1,v_2)
  p[ext,ret2](v_1,v_2) = 1/2
  foreach (zz in VarAll-{ret1,ret2}){
    p[inp,zz](v_1,v_2) = p[inp,zz](v_1,v_2)
    p[out,zz](v_1,v_2) = p[ext,zz](v_1,v_2)
    p[ext,zz](v_1,v_2) = 1/2
  }
}
// Cross Instrumentation
foreach (f in Fields){
  foreach(p in CrossInstrumField1){
    p[f,inp,out](v) = p[f,inp,ext](v)
    p[f,out,inp](v) = p[f,ext,inp](v)
    p[f,inp,ext](v) = 1/2
    p[f,ext,inp](v) = 1/2
    p[f,out,ext](v) = 1/2
    p[f,ext,out](v) = 1/2
  }
  foreach(p in CrossInstrumField2){
    p[f,inp,out](v_1,v_2) = p[f,inp,ext](v_1,v_2)
    p[f,out,inp](v_1,v_2) = p[f,ext,inp](v_1,v_2)
    p[f,inp,ext](v_1,v_2) = 1/2
    p[f,ext,inp](v_1,v_2) = 1/2
    p[f,out,ext](v_1,v_2) = 1/2
    p[f,ext,out](v_1,v_2) = 1/2
  }
}
foreach(p in CrossInstrum1){
  p[inp,out](v) = p[inp,ext](v)
  p[out,inp](v) = p[ext,inp](v)
  p[inp,ext](v) = 1/2
  p[ext,inp](v) = 1/2
  p[out,ext](v) = 1/2
  p[ext,out](v) = 1/2
}
foreach(p in CrossInstrum2){
  p[inp,out](v_1,v_2) = p[inp,ext](v_1,v_2)
  p[out,inp](v_1,v_2) = p[ext,inp](v_1,v_2)
  p[inp,ext](v_1,v_2) = 1/2
  p[ext,inp](v_1,v_2) = 1/2
  p[out,ext](v_1,v_2) = 1/2
  p[ext,out](v_1,v_2) = 1/2
}
})
    in begin
    blur(Y);
    coerce(Y);
    Y
    end
    end
  end
}


%%

// **********************************************************************
// EQUATIONS
// **********************************************************************

/* The program we want to analyze:

type cell = record
  n: ^cell;
  k: int; (* Abstracted *)
end record
type list = ^cell;

procedure main(list : list) is
var res,cell : list;
begin
main_entry:	(res,cell) := delete(list, (* k *));
main_end:
end

(* c is the deleted cell *)
function delete(h : list; (* k : int *)) : (t,c) is
begin
delete_entry:	if (h==NULL) then begin
delete1:		t := h
delete2:                c := NULL;
delete3
		end else begin
delete4:		t := h->n;
delete5:		if (? (* h->k==k *)) then begin
delete6:			h->n := NULL;
delete7:			c := h;
delete8:
			end else begin
delete9:			(t,c) := delete(t);
delete10:			h->n := NULL;
delete11:			h->n := t;
delete12:			t := h;
delete13:
			end
delete14:
		end
delete_end:
delete_summary:
end
*/

// main
main_entry	= Setup_1[list]			(main_begin)
main_end	= myret_2_1[res,cell,delete,list]	(main_entry,delete_summary)

// delete
delete_entry	= call_X_1[delete, list, h]	(main_entry)
delete_entry	= call_X_1[delete, t, h]	(delete5)
delete_entry_b  = BlurEntry[]			(delete_entry)
delete1		= IsVarNull[h]			(delete_entry_b)
delete2		= AssignVarVar[t,h]		(delete1)
delete3		= AssignVarNull[c]		(delete2)
delete4		= IsVarNotNull[h]		(delete_entry_b)
delete5		= AssignVarNext[t,h,n]		(delete4)
delete7		= AssignNextNull[h,n]		(delete5)
delete8		= AssignVarVar[c,h]		(delete7)
delete10	= myret_2_1[l,c,delete,t]	(delete5, delete_summary)
delete11	= AssignNextNull[h,n]		(delete10)
delete12	= AssignNextVar[h,n,l]		(delete11)
delete13	= AssignVarVar[t,h]		(delete12)

delete_end	= Identity[]		(delete3)
delete_end	= Identity[]		(delete8)
delete_end	= Identity[]		(delete13)

delete_summary_b = summary_1_2[delete,h,t,c]	(delete_end)
delete_summary	= BlurSummary[]			(delete_summary_b)

%%

main_entry
delete_entry
delete_entry_b
delete1
delete2
delete3
delete4
delete5
delete7
delete8
delete10
delete11
delete12
delete13
delete_end
delete_summary_b
delete_summary
main_end