GlobalDeclarations
{
var {:propertyMap} validFree : [int] bool;
//this is not being expanded
function {:inline} isValid(p : int, m : [int]bool) returns(bool) {m[p] || p == 0}
function {:ReachableStates} NonNULL(bool) : bool;
var {:AllocatorVar} freedp: int; //aliases every freed pointer
var {:AllocatorVar} freedNondet: bool;
procedure  freedNondetFn() returns (r:bool);
function {:inline} {:aliasingQuery} {:mkUniqueFn} aliasesWithFreed(p:int, q:int) returns (bool) {true}

procedure aliases(p1:int) {
    call freedNondet := freedNondetFn();
    goto L1, L2;
 
L1:
   assume p1 != NULL;
   freedp := if (freedNondet) then p1 else freedp;
   return;
 
L2: 
   return;
}

//checking the presence of extra procedures on instrumentation
procedure dontCareProc(x:int, y:int) returns (r:int){r := x + y; return;}

//a procedure that will be called from CorralExtraInit
procedure {:corralExtraInitExtension} cEIE() {
    assume (forall x:int :: validFree[x]); 
}

procedure boogie_si_record_bool(x:bool);

}


TemplateVariables
{
var p : int;
procedure {:#AnyArguments}  {:#NoImplementation} anyProc({:pointer} q : int) returns( {:#AnyParameters} r: int);
}


//Check every dereference is that of a allocated pointer
CmdRule
{
  assume {:nonnull} p != NULL;
}
-->
{
  #this;
  call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);
  assert (!aliasesWithFreed(p, freedp) || validFree[p] || p == 0); 
}

//Any parameter should be allocated
CmdRule
{
    call anyProc(p);
}
-->
{
    call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);
    assert (!aliasesWithFreed(p, freedp) || validFree[p] || p == 0); //the inlined function is not expanded
    #this;
}


//Any stub *[fF]ree* is considered a free
//Exclude methods such as RtlFreeUnicodeString that free fields
//ProcedureRule
//{
//    procedure {:#NameMatches "[fF]ree"} {:#NameNotMatches "^Rtl"} {:#NameNotMatches "Bogus"} {:#NoImplementation} builtin_free({:pointer} p : int);
//}
//-->
//{
//    validFree[p] := if (p == 0) then validFree[p] else false;
//    call aliases(p);
//}

//Narrowing free routines to only those that are known (10/30/17)
//free, _freea, _free_dbg, 
//ExFreePool, ExFreePoolWithTag, 
//Seen in true bugs: IoFreeMdl, 
//Not seen in true bugs: 
//IoFreeIrp
//LocalFree/GlobalFree: frees if the return is NULL (but used in many places without return)
//HeapFree(h, o, p): if the return is non-zero, then frees the 3rd arg
//VirtualFree:3 params/VirtualFreeEx:4 params. return non-zero for succes
//Not exposed in MSDN: SmfFreeMemory
//
//Add rules so that SDV can pick them up (sdv_ExFreePool) 

ProcedureRule
{
    //free is a Boogie keyword
    procedure  {:#NameMatches "^[fF]ree$"} builtin_free({:pointer} p : int);
    procedure  {:#NameMatches "^sdv_[fF]ree$"} builtin_free({:pointer} p : int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else false;
    call aliases(p);
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
    call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);
    return;
}

ProcedureRule
{
    procedure {:#ReplaceImplementation}  {:#NoImplementation} ExFreePool({:pointer} p : int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else false;
    call aliases(p);
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
    call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);
    return;
}

ProcedureRule
{
    //sdv-harness.c has a dummy definition for these guys, so we need to remove the implementation
    procedure {:#ReplaceImplementation}  sdv_ExFreePool({:pointer} p : int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else false;
    call aliases(p);
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
    call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);

    return;
}

ProcedureRule
{
    procedure {:#ReplaceImplementation}  {:#NoImplementation} ExFreePoolWithTag({:pointer} p : int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else false;
    call aliases(p);
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
    call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);
    return;
}

ProcedureRule
{
    //sdv-harness.c has a dummy definition for these guys, so we need to remove the implementation
    procedure {:#ReplaceImplementation}   sdv_ExFreePoolWithTag({:pointer} p : int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else false;
  call aliases(p);
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
      call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);  
    return;
}

ProcedureRule
{
    procedure {:#ReplaceImplementation}  {:#NoImplementation} IoFreeMdl({:pointer} p : int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else false;
    call aliases(p);
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
      call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);  
    return;
}

ProcedureRule
{
    //sdv-harness.c has a dummy definition for these guys, so we need to remove the implementation
    procedure {:#ReplaceImplementation}  sdv_IoFreeMdl({:pointer} p : int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else false;
    call aliases(p);
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
      call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);  
    return;
}


ProcedureRule
{
    procedure {:#ReplaceImplementation}  {:#NoImplementation} IoFreeIrp({:pointer} p : int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else false;
    call aliases(p);
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
      call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);  
    return;
}

ProcedureRule
{
    //sdv-harness.c has a dummy definition for these guys, so we need to remove the implementation
    procedure {:#ReplaceImplementation}  sdv_IoFreeIrp({:pointer} p : int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else false;
    call aliases(p);
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
      call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);  
    return;
}


ProcedureRule
{
    //https://msdn.microsoft.com/en-us/library/windows/desktop/aa366730(v=vs.85).aspx
    procedure {:#ReplaceImplementation}  {:#NoImplementation} LocalFree({:pointer} p : int) returns (r:int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else (validFree[p] && r != 0);
    call aliases(p); //ok to alias with freed pointer since r happens non-deterministically
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
      call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);  
    return;
}

ProcedureRule
{
    //sdv-harness.c has a dummy definition for these guys, so we need to remove the implementation
    //https://msdn.microsoft.com/en-us/library/windows/desktop/aa366730(v=vs.85).aspx
    procedure {:#ReplaceImplementation}   sdv_LocalFree({:pointer} p : int) returns (r:int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else (validFree[p] && r != 0);
    call aliases(p); //ok to alias with freed pointer since r happens non-deterministically
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
      call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);  
    return;
}

ProcedureRule
{
    //https://msdn.microsoft.com/en-us/library/windows/desktop/aa366579(v=vs.85).aspx
    procedure {:#ReplaceImplementation}  {:#NoImplementation} GlobalFree({:pointer} p : int) returns (r:int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else (validFree[p] && r != 0);
    call aliases(p); //ok to alias with freed pointer since r happens non-deterministically
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
      call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);  
    return;
}

ProcedureRule
{
    //sdv-harness.c has a dummy definition for these guys, so we need to remove the implementation
    //https://msdn.microsoft.com/en-us/library/windows/desktop/aa366579(v=vs.85).aspx
    procedure {:#ReplaceImplementation}   sdv_GlobalFree({:pointer} p : int) returns (r:int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else (validFree[p] && r != 0);
    call aliases(p); //ok to alias with freed pointer since r happens non-deterministically
    assert {:sourcefile "?"} {:sourceline 0} {:print "Return"} true;
      call {:cexpr "freed-pointer"} boogie_si_record_bool(!validFree[p]);  
    return;
}

