/* A Tvp program for reverse

*/

#define COMPLETE

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

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

%s InsertVar	{h,c,t}

%s MainVar	{ list,cell,res }

%s VarAll	InsertVar + MainVar

%s Fields { n }
%s Bools { }

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

// ====================================================================== 
// 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,fp2} ){
      %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,fp2}){
      %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" 

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

%function BlurSuccPred[](X)
    %t "BlurSuccPred"
{
  begin
    let Y = transform(X,
	update:{
foreach (m in Mode){
  foreach (f in Fields){
    foreach (z in VarAllFPR){
      foreach (p in {succ,pred}){
        p[f,m,z](v) = 1/2
      }
    }
  }
}
sm(v) = 1/2
})
    in begin
      blur(Y);
      coerce(Y);
      Y
    end
  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), r[n,out,c](v) });
    let Y = transform(X,
	update:{
sm(v) = ( (r[n,out,h](v) | r[n,out,c](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), r[n,out,fp2](v) });
    let Y = transform(X,
	update:{
sm(v) = ( (r[n,out,fp1](v) | r[n,out,fp2](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);
      Y
    end
  end
}

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

/* This due to the fact that one add a cell in a list, which "creates a new
   pattern from scratch", ulike list reversal. */

%function myret_1_2[ret1, name, act1, act2](Xcaller,Xcallee)
     %t "MyRet_1_2 " + ret1 + " := " + name + "(" + act1 + ", " + act2 + ")"
{
  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
// We equate fp1 to act1 in Xcaller
fp1(v) = act1(v)
fp2(v) = act2(v)
foreach (f in Fields){
  foreach (p in InstrumFieldVar1){ 
    p[f,out,fp1](v) = p[f,out,act1](v) 
    p[f,out,fp2](v) = p[f,out,act2](v) 
  }
  foreach (p in InstrumFieldVar2){ 
    p[f,out,fp1](v_1,v_2) = p[f,out,act1](v_1,v_2) 
    p[f,out,fp2](v_1,v_2) = p[f,out,act2](v_1,v_2) 
  }
}
foreach (p in InstrumModeVar1){ 
  p[out,fp1](v) = p[out,act1](v) 
  p[out,fp2](v) = p[out,act2](v) 
}
foreach (p in InstrumModeVar2){ 
  p[out,fp1](v_1,v_2) = p[out,act1](v_1,v_2) 
  p[out,fp2](v_1,v_2) = p[out,act2](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,fp2,fr1}){
      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,fp2,fr1}){
    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), succ[n,ext,fp2](v), pred[n,ext,fp2](v), r[n,ext,fp2](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)
fp1(v) = 1/2
fp2(v) = 1/2
fr1(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
    foreach (zz in VarAll-{ret1}){
      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
    foreach (zz in VarAll-{ret1}){
      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
  foreach (zz in VarAll-{ret1}){
    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
  foreach (zz in VarAll-{ret1}){
    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; cell : list) is
var res : list;
begin
main_entry:	res := insert(list, cell);
main_end:
end

(* c is supposed to be a list with one element (eg, with c->n := NULL) *)
function insert(h : list; c : list) : t is
begin
insert_entry	if (h!=NULL && ? (* h->k < c->k *)) then begin
insert1			t := h->n;
insert2			t := insert(t,c);
insert3			h->n := NULL;
insert4			h->n := t;
insert5                 t := h
insert6
		end else begin
insert7			c->n := h;
insert8			t := c;
insert9
		end
insert_end
insert_summary
end
*/


// main
main_entry	= Setup_2[list,cell]		(main_begin)
main_end	= myret_1_2[res,insert,list,cell]	(main_entry,insert_summary)
// insert
insert_entry	= call_X_2[insert, list, cell, h, c]	(main_entry)
insert_entry	= call_X_2[insert, t, c, h, c]		(insert2)
insert_entry_b  = BlurEntry[]				(insert_entry)
insert1		= IsVarNotNull[h]			(insert_entry_b)
insert2		= AssignVarNext[t,h,n]			(insert1)
insert3		= myret_1_2[t,insert,t,c]	       	(insert2,insert_summary)
insert4		= AssignNextNull[h,n]			(insert3)
insert5		= AssignNextVar[h,n,t]			(insert4)
insert6		= AssignVarVar[t,h]			(insert5)

insert8		= AssignNextVar[c,n,h]			(insert_entry_b)
insert9		= AssignVarVar[t,c]			(insert8)

insert_end	= Identity[]			(insert6)
insert_end	= Identity[]			(insert9)
insert_summary_b  = summary_2_1[insert,h,c,t]		(insert_end)
insert_summary	= BlurSummary[]				(insert_summary_b)


%%

main_entry
insert_entry
insert_entry_b
insert1
insert2
insert3
insert4
insert5
insert6
insert8
insert9
insert_end
insert_summary_b
insert_summary
main_end