// --- DefUse --------------------------------------------------------------------------------------
// a variable x defined at label def_l is used at label use_l
// def_ and use_ define def and use without the added assign_() predicates
// uses ReachingDef

.decl def_(l:label, x:var)
def_(l, x) :- source(l, x).
def_(l, x) :- assign(l, x, _, _).

.decl def(l:label, x:var)
//.output def
def(l, x) :- def_(l, x).
def(l, x) :- assign_(l, x).

.decl use_(l:label, x:var)
use_(l, x) :- sink(l, x).
use_(l, x) :- assign(l, _, x, _).
use_(l, x) :- assign(l, _, _, x).
use_(l, x) :- if(l, _, x, _).
use_(l, x) :- if(l, _, _, x).

.decl use(l:label, x:var)
//.output use
use(l, x) :- use_(l, x).
use(l, x) :- assign_(l, x).


.decl def_use(def_l:label, use_l:label, x:var, c:chain, t:trace)
//.output def_use
def_use(def_l, use_l, x, cat( cat("_*", cat(def_l, x)), cat("+", cat(use_l, x))), t) :- def(def_l, x), use(use_l, x), reaching_def(def_l, use_l, x, t), def_l != use_l.


// list labels on the def-use trace; excluding def_l, but including use_l (-> potential sanitize locations)
.decl def_use_labels(def_l:label, use_l:label, x:var, l:label, c:chain, t:trace)
//.output def_use_labels
def_use_labels(def_l, use_l, x, l, c, t) :- def_use(def_l, use_l, x, c, t), reaching_def(def_l, l, x, t), equal_or_earlier(l, use_l).


// --- DefUseChain: includes the potential candidate labels and variables ---
.decl def_use_chain(def_l:label, def_x:var, use_l:label, use_x:var, candidate_l:label, candidate_x:var, c:chain, t:trace)
//.output def_use_chain
def_use_chain(def_l, x, use_l, x, l, x, c, t) :- def_use_labels(def_l, use_l, x, l, c, t).

def_use_chain(def_l, def_x, use_l, use_x, l1, x1, cat(c1, c2), t) :- def_use_chain(def_l, def_x, l, y, l1, x1, c1, t), assign(l, x, y, _), def_use_chain(l, x, use_l, use_x, _, _, c2, t), contains(cat("_", l), t).
def_use_chain(def_l, def_x, use_l, use_x, l2, x2, cat(c1, c2), t) :- def_use_chain(def_l, def_x, l, y, _, _, c1, t), assign(l, x, y, _), def_use_chain(l, x, use_l, use_x, l2, x2, c2, t), contains(cat("_", l), t).

def_use_chain(def_l, def_x, use_l, use_x, l1, x1, cat(c1, c2), t) :- def_use_chain(def_l, def_x, l, z, l1, x1, c1, t), assign(l, x, _, z), def_use_chain(l, x, use_l, use_x, _, _, c2, t), contains(cat("_", l), t).
def_use_chain(def_l, def_x, use_l, use_x, l2, x2, cat(c1, c2), t) :- def_use_chain(def_l, def_x, l, z, _, _, c1, t), assign(l, x, _, z), def_use_chain(l, x, use_l, use_x, l2, x2, c2, t), contains(cat("_", l), t).

def_use_chain(def_l, def_x, use_l, use_x, l1, x1, cat(c1, c2), t) :- def_use_chain(def_l, def_x, l, x, l1, x1, c1, t), assign_(l, x), def_use_chain(l, x, use_l, use_x, _, _, c2, t), contains(cat("_", l), t).
def_use_chain(def_l, def_x, use_l, use_x, l2, x2, cat(c1, c2), t) :- def_use_chain(def_l, def_x, l, x, _, _, c1, t), assign_(l, x), def_use_chain(l, x, use_l, use_x, l2, x2, c2, t), contains(cat("_", l), t).