TXL solution to TIL Chairmarks #4.5: Static slicing. This example implements backward static slicing using cascaded markup to a fixed point.

-- JamesCordy - 02 Mar 2007

File "TILbackslice.Txl"

% Backward static slicing of Tiny Imperative Language programs
% Jim Cordy, February 2007

% Given a TIL program with a single statement marked up using the
% XML markup <mark> </mark>, backward slices the program from that
% statement and its referenced variables.

% Works by inducing markup of unmarked statements from already marked-up
% statements beginning with the original marked statement until a fixed 
% point is reached, then removing all remaining unmarked statements.
% No dependency graph is required.

% Begin with the TIL base grammar
include "TIL.Grm"

% Add allowance for XML markup of TIL statements
redefine statement
        ...
    |   [marked_statement]
end redefine

define marked_statement
            [xmltag] [statement] [xmlend]
end define

define xmltag
        < [SPOFF] [id] > [SPON]
end define

define xmlend
        < [SPOFF] / [id] > [SPON]
end define

% Conflate while and for statements into one form to optimize
% handling of both forms in one rule
redefine statement
        [loop_statement]
    |   ...
end redefine

define loop_statement
        [loop_head]                [NL][IN]
            [statement*]           [EX]
        'end                       [NL]
end define

define loop_head
        while [expression] do
    |   for [id] := [expression] to [expression] do
end define


% The main function gathers the steps of the transformation:
% induce markup to a fixed point, remove unmarked statements,
% remove declarations for variables not used in the slice,
% and strip the markups to yield the sliced program

function main
    replace [program]
        P [program]
    by
        P [propogateMarkupToFixedPoint]
          [removeUnmarkedStatements]
          [removeRedundantDeclarations]
          [stripMarkup]
end function

% Back propogate markup of statements beginning with the initially
% marked statement of interest.  Continue until a fixed point, 
% when no new markups are induced

rule propogateMarkupToFixedPoint
    replace [program]
        P [program]

    construct NP [program]
        P [backPropogateAssignments]
          [backPropogateReads]
          [whilePropogateControlVariables]
          [loopPropogateMarkup]
          [loopPropogateMarkupIn]
          [ifPropogateMarkupIn]
          [compoundPropogateMarkupOut]

    % We're at a fixed point when P = NP   :-)
    deconstruct not NP
        P
    by
        NP 
end rule

% Rule to back-propogate markup of assignments.
% A previous assignment is in the slice if its assigned 
% variable is used in a following marked statement

rule backPropogateAssignments
    skipping [marked_statement]
    replace [statement*]
        X [id] := E [expression] ; 
        More [statement*]
    where 
        More [hasMarkedUse X]
    by
        <mark> X := E; </mark>
        More 
end rule

% Similar rule for back-propogating markup of read statements

rule backPropogateReads
    skipping [marked_statement]
    replace [statement*]
        read X [id] ; 
        More [statement*]
    where 
        More [hasMarkedUse X]
    by
        <mark> read X; </mark>
        More 
end rule

function hasMarkedUse X [id]
    match * [marked_statement]
        M [marked_statement]
    deconstruct * [expression] M
        E [expression]
    deconstruct * [id] E
        X
end function

% Assignments to variables inside a while loop containing statements
% of a slice are also in the slice if the while condition uses them

rule whilePropogateControlVariables
    replace $ [statement]
        while E [expression] do
            S [statement*]
        'end
    deconstruct * [statement] S
        _ [marked_statement]
    by
        while E do
            S [markAssignmentsTo E]
              [markReadsOf E]
        'end
end rule

rule markAssignmentsTo Exp [expression]
    skipping [marked_statement]
    replace $ [statement]
        X [id] := E [expression] ;
    deconstruct * [id] Exp
        X
    by
        <mark> X := E; </mark>
end rule

rule markReadsOf Exp [expression]
    skipping [marked_statement]
    replace $ [statement]
        read X [id] ;
    deconstruct * [id] Exp
        X
    by
        <mark> read X; </mark>
end rule

% Rule for propagating dependencies around loops.
% An assignment inside a loop is in the slice if its assigned variable
% is used in a marked statement anywhere inside the loop

rule loopPropogateMarkup
    replace $ [statement]
        Head [loop_head]
            S [statement*]
        'end
    construct MarkedS [marked_statement*]
        _ [^ S]
    construct MarkedE [expression*]
        _ [^ MarkedS]
    by
        Head
            S [markAssignmentsTo each MarkedE]
              [markReadsOf each MarkedE]
        'end
end rule

% Rule for propagating dependencies into loops.
% An assignment inside the loop is in the slice if its assigned variable 
% is used in a marked statement anywhere following the loop

rule loopPropogateMarkupIn
    replace $ [statement*]
        Head [loop_head]
            S [statement*]
        'end
        MoreS [statement*]
    construct MarkedMoreS [marked_statement*]
        _ [^ MoreS]
    construct MarkedMoreE [expression*]
        _ [^ MarkedMoreS]
    by
        Head
            S [markAssignmentsTo each MarkedMoreE]
              [markReadsOf each MarkedMoreE]
        'end
        MoreS
end rule

% Rule for propagating dependencies into if statements.
% An assignment inside the then or else part of the if is in the slice 
% if its assigned variable is used in a marked statement anywhere 
% following the if

rule ifPropogateMarkupIn
    replace $ [statement*]
        if E [expression] then
            ST [statement*]
        ElseSE [opt else_statement]
        'end
        MoreS [statement*]
    construct MarkedMoreS [marked_statement*]
        _ [^ MoreS]
    construct MarkedMoreE [expression*]
        _ [^ MarkedMoreS]
    by
        if E then
            ST [markAssignmentsTo each MarkedMoreE]
        ElseSE [markAssignmentsTo each MarkedMoreE]
        'end
        MoreS
end rule

% Rule for propagating dependencies out.
% A compound statement of any kind is in the loop if it contains
% a marked statement

rule compoundPropogateMarkupOut
    replace $ [statement*]
        CS [statement]
        More [statement*]
    deconstruct not CS
        _ [marked_statement]
    deconstruct * [statement] CS
        _ [marked_statement]
    by
        <mark> CS </mark>
        More
end rule

% Rule to remove all unmarked statements after the fixed point
% is reached, yielding only the slice

rule removeUnmarkedStatements
    replace [statement*]
        S [statement]
        More [statement*]
    deconstruct not S
        _ [marked_statement]
    deconstruct not S
        _ [declaration]
    by
        More
end rule

% Rule to remove declarations not needed in the slice

rule removeRedundantDeclarations
    replace [statement*]
        var X [id] ;
        More [statement*]
    deconstruct not * [id] More
        X
    by
        More
end rule

% Rule to strip all markup when we're done

rule stripMarkup
    replace [statement]
        < _ [id] > S [statement] </ _ [id] >
    by
        S
end rule

Example run 1:

<linux> cat sliceg1.til
var n;
read n;
var fac;
fac := 1;
var sum;
sum := 0;
var i;
i := 1;
while i != n+1 do
    fac := fac * i;
    sum := sum + i;
    i := i + 1;
end
<foo>write fac;</foo>
write sum;

<linux> txl sliceg1.til TILbackslice.Txl
TXL v10.4d (4.2.07) (c)1988-2007 Queen's University at Kingston
Compiling TILbackslice.Txl ... 
Parsing sliceg1.til ...
Transforming ...
var n;
read n;
var fac;
fac := 1;
var i;
i := 1;
while i != n + 1 do
    fac := fac * i;
    i := i + 1;
end
write fac;

<linux>

Example run 2:

<linux> cat sliceg2.til 
var x;
x := 0;
var t;
t := 0;
for i := 1 to 10 do
    if x = 1 then
        t := t * i;
    else
        t := t + i;
    end
    x := 1;
end
<mark>write x;</mark>

<linux> txl sliceg2.til TILbackslice.Txl
TXL v10.4d (4.2.07) (c)1988-2007 Queen's University at Kingston
Compiling TILbackslice.Txl ... 
Parsing sliceg2.til ...
Transforming ...
var x;
x := 0;
for i := 1 to 10 do
    x := 1;
end
write x;

<linux> 

Example run 3:

<linux> cat sliceg6.til
var lines;
lines := 0;    
var chars;    
var n;    
read n;
var eof_flag;
read eof_flag;
chars := n;   
while eof_flag do
    lines := lines + 1;     
    read n;
    read eof_flag;
    chars := chars + n;   
end
<mark>write (lines);</mark>
write (chars);

<linux> txl sliceg6.til TILbackslice.Txl
TXL v10.4d (4.2.07) (c)1988-2007 Queen's University at Kingston
Compiling TILbackslice.Txl ... 
Parsing sliceg6.til ...
Transforming ...
var lines;
lines := 0;
var eof_flag;
read eof_flag;
while eof_flag do
    lines := lines + 1;
    read eof_flag;
end
write (lines);

<linux>

-- JamesCordy - 02 Mar 2007