//--------------------------------------------------------------------------------------------------
// NOTE: this code is only for illustrative purpose. It's from an earlier version of the analyzer
// that still worked with the original CFG definitions by follows(). But the basic algorithms apply.
// Later versions of the analyzer moved to a mapped_follows() definition of the CFG to avoid
// distinguishing between first and second if condition at multiple analysis locations.
// Some of the problems of the original CGF definition already show here (special case handlings)
// Thus, the introduction of the mapped CFG in the analyzer.
//--------------------------------------------------------------------------------------------------

// --- blocks: trace segments of the same branch ---------------------------------------------------
// defines code blocks (see basic block analysis from compiler design) to simplify finding unified locations for sanitize()
// reasoning: sorting/picking first/last of a selection of candidates is tricky and lead to
// cyclic negations during testing. Using unified candidate locations at start or end of blocks leads to
// automatic collapse of some of the candidates. No sorting needed anymore.
// These pre-defined predicates allow simple lookup operations.

// begin: as common in block analysis, it is correct that the if condition itself is part of the
// upper block (i.e. as last element of it); here 2 if conditions (if and else), which is OK.
// They are only used as lookups.
// technical note: deduced in forward analysis
.decl block_begin_(begin_l:label, lookup_l:label)
block_begin_(l, l) :- first(l).
block_begin_(d, d) :- if(_, d, _, _).
block_begin_(j, j) :- join(j, _, _).
block_begin_(b, l2) :- block_begin_(b, l1), follows(l2, l1), !if(_, l2, _, _), !join(l2, _, _).

// end: here it is crucial to ignore the 2nd if condition (else) and only keep the first one (true if)
// technical note: deduced in backward analysis
.decl block_end_(end_l:label, lookup_l:label)
block_end_(l, l) :- last(l).
block_end_(b, b) :- join(_, b, _).
block_end_(b, b) :- join(_, _, b).
block_end_(i, i) :- if(i, _, _, _), is_first_if(i).  // do not keep if condition for else branch here
block_end_(e, l1) :- block_end_(e, l2), follows(l2, l1), !join(_, l1, _), !join(_, _, l1), !if(l1, _, _, _).

// summarizing
.decl block(begin_l:label, end_l:label, lookup_l:label)
.output block
block(begin_l, end_l, lookup_l) :- block_begin_(begin_l, lookup_l), block_end_(end_l, lookup_l).

// find the block before or after the current block
// to simplify lookup, any label within a block will work as lookup_l
// note: this may give one or two blocks (see branches in if conditions)
.decl earlier_block(begin_l:label, end_l:label, lookup_l:label)
.output earlier_block
earlier_block(begin_l, end_l, lookup_l) :- block(b, _, lookup_l), follows(b, e), block(begin_l, end_l, e).

// note: the special case of if conditions must be handled -> both branches are following
.decl later_block(begin_l:label, end_l:label, lookup_l:label)
.output later_block
later_block(begin_l, end_l, lookup_l) :- block(_, e, lookup_l), !if(e, _, _, _), follows(b, e), block(begin_l, end_l, b).
later_block(begin_l, end_l, lookup_l) :- block(_, e, lookup_l), if(e, _, _, _), find_first_if(e, first), follows(b, first), block(begin_l, end_l, b).
later_block(begin_l, end_l, lookup_l) :- block(_, e, lookup_l), if(e, _, _, _), find_second_if(e, second), follows(b, second), block(begin_l, end_l, b).