TXL solution to [[TIL Chairmarks]] #4.5: Static slicing. This example implements backward static slicing using cascaded markup to a fixed point. *Notes:* In an implementation for a real scoped language, a unique renaming transformation would normally be done before slicing in order to remove ambiguities of reference. Alias resolution may or may not be necessary depending on the language. Inter-procedural slicing is added in the usual way, by marking the formal parameters corresponding to any argument variable of the slice passed by reference to the procedure. -- Main.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 , 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 X := E; 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 read X; 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 X := E; end rule rule markReadsOf Exp [expression] skipping [marked_statement] replace $ [statement] read X [id] ; deconstruct * [id] Exp X by read X; 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 CS 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] by S end rule _Example run 1:_ 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 write fac; write sum; 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; _Example run 2:_ 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 write x; 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; _Example run 3:_ 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 write (lines); write (chars); 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); -- Main.JamesCordy - 02 Mar 2007