CISC422/853: Formal Methods in Software Engineering: Computer-Aided Verification (Winter 2009) Assignment 4 (Slicing) Due Fri, April 3, 2009

In this assignment, you will implement static backward slicing (as discussed in class) for IMP programs. More precisely, you will complete provided Java code such that it computes and outputs the slice of a IMP program.

1. Provided code: Download the code here into some directory d and unpack it. Add d to your classpath.
2. IMP programs: The above code contains a parser for IMP programs with locations. The grammar of IMP programs is

         // This is the grammar for a simple, imperative language
         // called IMP in Backus-Naur Form (BNF). 
         // Keywords can be used in lower case or upper case.
         // This grammar is implemented in parser/imp1.cup.
         // The parser is generated automatically using java_cup.
         [program] ::=                  PROGRAM [id] ;
                                        [var_decl_section]
                                        BEGIN
                                        [stmt_list]
                                        END
         [var_decl_section] ::=         VAR [var_decl_list] | [empty]
         [var_decl_list] ::=            [var_decl] ; [var_decl_list] | [var_decl]
         [var_decl] ::=                 [id] : [basic_type]
         [basic_type] ::=               int | bool
         [stmt_list] ::=                [stmt] ; [stmt_list] | [stmt] | [empty]
         [stmt] ::=                     [skip] | [assignment] | [cond] | [while] | [repeat] | [print]
         [skip] ::=                     [loc] SKIP
         [assignment] ::=               [loc] [var] := [exp]
         [cond] ::=                     [loc] IF [exp] THEN [stmt_list] [loc] END |
                                        [loc] IF [exp] THEN [stmt_list] ELSE [stmt_list] [loc] END
         [while] ::=                    [loc] WHILE [exp] DO [stmt_list] [loc] END
         [repeat] ::=                   [loc] REPEAT [stmt_list] [loc] UNTIL [exp]
         [print] ::=                    [loc] PRINT ([exp])
         [loc] ::=                      [num] :
         [exp] ::=                      [id] | [num] | [bool] |
                                        ([exp]) | [unary_op] [exp] | [exp] [binary_op] [exp]
         [unary_op] ::=                 - | !
         [binary_op] ::=                + | - | * | / | && | || | = | < | <=
         [id] ::=                       identifer
         [num] ::=                      number
         [bool] ::=                     true | false
         [empty] ::=
         

   Here's an example of an syntactically well-formed IMP program:

         PROGRAM p7;
         VAR
                   n : INT;
                   i : INT;
                   x : INT;
                   y : INT
         0: BEGIN
         1:        n := 1;
         2:        i := 1;
         3:        x := 0;
         4:        y := 0;
         5:        WHILE i <= (n - 1) DO
         6:                x := x + i;
         7:                y := y + i;
         8:                i := i + 1
         9:        END;
         10:       x := x + n;
         11:       y := y + n
         12: END
         

   Note that a ";" functions as a statement separator (as in Pascal, for instance), rather than a statement terminator (as in C or Java). You can find more IMP programs in d/imp/testPrograms and d/imp/moreTestPrograms.
3. Structure of the provided code: The code consists of 7 packages:
   • imp: This is the top-level package. It contains two Java files:
     • imp.main.java: This file contains contains the main method. It reads in the location of the IMP to be sliced and the criterion variables as command line arguments, reads in the IMP program, and then parses the input. If it is syntactically correct, the corresponding abstract syntax tree (AST) and the control flow graph (CFG) are computed. The invocation

       		  cfg.computeSlice(cNode, cVars);
       		  

       then is supposed to compute the slice using the criterion variables passed in as arguments and the last node of the program (that is, the final END node) as criterion node. The invocation cfg.toStringUsingRelevant() will produce a string representation of the slice by using the isRelevant attribute: The string representation of a node is included in the slice only if its isRelevant attribute is set.
     • imp.test.java:: Contains some code to explore the Control Flow Graph. May help you to get started by illustrating by example how to access the CFG, but it is not necessary in any way and you can ignore it.
   • imp.testPrograms: This package contains 11 IMP programs you must use for testing.
   • imp.moreTestPrograms: This directory contains more IMP programs you can use for testing.
   • imp.parser: This package contains the code for the parsing, that is, the conversion of the program into an internal Abstract Syntax Tree (AST). In general, we have a class for each non-terminal symbol in the grammar (e.g., StmtList, AssignStmt). The CFG is created by invoking toCfg() on the AST. The routine works as outlined in the slicing notes on the Readings Page.
   • imp.slicer: This package contains the code for the slicer. The classes whose names end in "Node" all are used to represent nodes in the CFG. Every node has a nexts and a prevs attribute. These store, respectively, the successors and predecessors of the node. Moreover, a node has a isRelevant attribute.
     With respect to methods, every node has a

     	    computeDRVars(Node cNode, VarIdSet cVars)
     	    

     method which computes the variables directly relevant at the node. The method stores the relevant variables in the attribute dRVars. It will also set the isRelevant attribute, if the node is found to be directly relevant. Moreover, a node has a method toStringUsingRelevant which is used to "unparse" the relevant portions of the AST (i.e. convert back into string form and output).
   • imp.util: This package contains two classes. One is VarIdSet which defines the data structure in which the relevant variables are stored. The other is a general utility package containing various helper methods.
   • imp.java_cup: This package contains all the code necessary to parsing IMP programs. The code for the lexical analysis was automatically generated using the JLex lexical analyzer generator on the definition file d/imp/parser/imp1.lex. The code for the parser was automatically generated using the CUP parser generator on the definition file d/imp/parser/imp1.cup.
4. Your task: Following the discussion of slicing in class and the notes on slicing on the Readings page as a guideline, your task is to complete the provided code in package imp.slicer such that it implements static backwards slicing for IMP programs. To this end, you need to:
   1. Make sure that the provided code above compiles. It should compile fine. To do this, you can use whatever Java programming environment you like (e.g., JBuilder, Eclipse, etc). But you can also do this from the command-line. Under Cygwin, the following worked for me:

      	    $ pwd
      	    /home/Juergen Dingel/teaching/cisc853_F06/assignments/A3/imp
      	    $ javac -classpath "c:\cygwin\home\Juergen Dingel\teaching\cisc853_F06\assignments\A3" *.java parser/*.java util/*.java
      	    

      That is, invoke javac from directory d/imp with d in your class path.
   2. Run the compiled code. Again, use whatever environment you are comfortable with. To run the program from the command-line, change to directory d, and invoke the program with, for instance, java imp.Main imp/testPrograms/p1.imp x y. Again, under Cygwin:

      	    $ cd ..
      	    $ pwd
      	    /home/Juergen Dingel/teaching/cisc853_F06/assignments/A3
      	    $ java imp.Main imp/testPrograms/p1.imp x
      	    Reading Imp program from file imp/testPrograms/p1.imp
      	    ...
      	    

      That is, invoke imp.Main from directory d. Note that you only need to provide the file name and the criterion variables as command-line arguments. The criterion location will always be the last node in the program. When run, the provided code should display the original program and the slicing criteria correctly. However, the slice will always consist of just the first and the last node.
   3. Understand the provided code. In particular, you need to understand how the various IMP control constructs (e.g., if-then, if-then-else, while, repeat) are represented in the CFG. To understand this, take a look at the toCFG method for each construct. For instance, the toCFG method in class IfThenElseStmt will tell you how an if-then-else statement is represented in as a CFG. Also, the file test.java in package imp contains some sample code showing you how to access the CFG.
   4. To make the code compute the slice correctly, modify the code as follows:
      1. Every node has a dRVars attribute used to store the directly relevant variables. This attribute has type VarIdSet. To query and manipulate dRVars, you have to complete the implementation of VarIdSet appropriately. The template code for VarIdSet sits in the imp.util package.
      2. Complete the code for the method computeDRVars for the various nodes defined in imp.parser. It is best if you proceed in stages:
         1. First, deal with programs in which the control flow cannot branch or loop. In other words, programs that do not contain if-then, if-then-else, while, or repeat statements. In this setting, you need to modify the computeDRVars methods for AssignNode, SkipNode, and PrintNode such that it
            • computes the directly relevant variables (dRVars) of the node,
            • determines if the node is relevant and if so, mark it as such by setting the boolean attribute isRelevant,
            • calls computeDRVars on all predecessors.
            Note that for ProgramEndNode the second step is not necessary, because the toStringUsingRelevant method in Cfg.java used to print the slice will always print the ProgramBeginNode and the ProgramEndNode.
         2. Next, deal with if-then statements. Modify the computeDRVars method in IfThenTestNode and TestEndNode such that the directly relevant variables are computed. Once you're done with that deal with if-then-else statements.
         3. Now, allow looping in your programs by adding while and repeat statements. For each, you will need to implement the "fixed point" computation discussed in class.
      You may modify any of the provided classes as you see fit, but you should really only have to modify code in the imp.slicer package.
   5. Document the code that you add in an appropriate way.
   6. Test your implementation on at least the 11 IMP programs p1.limp through p11.limp provided in the package imp.testPrograms.
5. Hand in:
   1. Printouts of the files that you added or modified.
   2. Run 22 tests T.1.a, T.1.b, T.2.a, T.2.b to T.11.a, T.11.b. In test T.i.a slice imp/testPrograms/pi.imp with respect to the criterion variables Va = {x}. In test T.i.b slice imp/testPrograms/pi.imp with respect to the criterion variables Va = {y}. For each test, hand in a printout of the sliced program.
   3. Extra Question: Let P be a IMP program and V1 and V2 sets of criterion variables. Let "slice(P,V)" denote the slice of P with respect to (n, V) where n is the last node in P and V is a set of variables. Moreover, let "slice(P,V1) union slice(P,V2)" denote the slice of P that contains a node i iff i is either in slice(P,V1) or in slice(P,V2). Similarly for "slice(P,V1) intersect slice(P,V2)". Consider the following equations:
      1. slice(P, V1 union V2) = slice(P, V1) union slice(P, V2)
      2. slice(P, V1 intersect V2) = slice(P, V1) intersect slice(P, V2)
      For each of the equations, decide if it holds or not for any P, V1, and V2. If you think the equation holds, write down "yes" and include a brief, informal, yet convincing argument why you think it holds. If you think the equation does not hold, write "no" and include a counter example, that is, a IMP program P and sets of criterion variables V1 and V2 such that the equation fails.
6. Hints, remarks:
   • Marking criteria: The correctness, comprehensibility, and readability of your code will be used as marking criteria.
   • Parser generators: The use of lexer and parser generators is very common in industry. Other parser generators for Java are javacc and ANTLR. Generators for C under Unix include lex and yacc.
   • Editing IMP programs: If you write an IMP program completely from scratch, the parser may reject it even if it is well-formed by complaining about "Unmatched Input". This problem typically occurs with Windows-based editors. The reason is that line breaks are represented differently under Windows and this trips up the parser. To solve this problem, there are several options: Edit an existing program under Windows but without introducing line breaks, edit using a Unix- or Cygwin-based editor, or write your IMP program without line breaks.