prop-src/prog.pC

   1 /////////////////////////////////////////////////////////////////////////////
   2 //  This test implements a rewrite based simplifier for the abstract
   3 //  syntax of a toy imperative language.
   4 /////////////////////////////////////////////////////////////////////////////
   5 #include <iostream>
   6
   7 /////////////////////////////////////////////////////////////////////////////
   8 //  The following recursive type equations define the abstract syntax
   9 //  of our small language.
  10 //  ( Note: we define our own boolean type because not all C++ compilers
  11 //    have bool built-in yet. )
  12 /////////////////////////////////////////////////////////////////////////////
  13 datatype List<T> = #[]                             // a polymorphic list
  14                  | #[ T ... List<T> ]
  15
  16 and      BOOL    = False | True                    // a boolean type
  17
  18 and      Exp     = integer ( int )                 // integers
  19                  | real    ( double )              // real numbers
  20                  | string  ( char * )              // strings
  21                  | boolean ( BOOL )                // booleans
  22                  | binop   ( BinOp, Exp, Exp )     // binary op expression
  23                  | unaryop ( UnaryOp, Exp )        // unary op expression
  24                  | var     ( Id )                  // variables
  25
  26 and      BinOp   = add | sub | mul | divide | mod  // binary operators
  27                  | logical_and | logical_or
  28                  | eq  | ge | le | lt | gt | ne
  29
  30 and      UnaryOp = uminus | logical_not            // unary operators
  31
  32 and      Stmt    = assign_stmt ( Id, Exp )                // assignments
  33                  | while_stmt  ( Exp, Stmt )              // while statements
  34                  | if_stmt     ( Exp, Stmt, Stmt )        // if statements
  35                  | print_stmt  ( Exp )                    // print statements
  36                  | block_stmt  ( List<Decl>, List<Stmt> ) // blocks
  37
  38 and      Type    = primitive_type ( Id )                  // type expressions
  39                  | pointer_type   ( Type )
  40                  | array_type     { element : Type, bound : Exp }
  41                  | function_type  { arg : Type, ret : Type }
  42                  | tuple_type     ( List<Type> )
  43                  | record_type    ( List<LabeledType> )
  44
  45 and      Decl    = decl { name : Id, typ : Type }        // declarations
  46
  47 and  LabeledType = labeled_type (Id, Type)               // labeled types
  48
  49 where type Id    = const char *
  50 ;
  51
  52 /////////////////////////////////////////////////////////////////////////////
  53 //  Refine the implementation of the datatypes.
  54 //  The qualifiers may be also declared in the datatype definition.
  55 //  We qualify the datatypes here so that they won't clutter up
  56 //  the equations above.
  57 //
  58 //  All types are declared to be printable by
  59 //  the printer method and rewritable.
  60 /////////////////////////////////////////////////////////////////////////////
  61 refine List<T>     :: printable rewrite
  62 and    BOOL        :: printable rewrite
  63 and    Exp         :: printable rewrite
  64 and    BinOp       :: printable rewrite
  65 and    UnaryOp     :: printable rewrite
  66 and    Stmt        :: printable rewrite
  67 and    Type        :: printable rewrite
  68 and    Decl        :: printable rewrite
  69 and    LabeledType :: printable rewrite
  70
  71 /////////////////////////////////////////////////////////////////////////////
  72 //  Specify the pretty printing formats.
  73 /////////////////////////////////////////////////////////////////////////////
  74 and printable
  75     False          => "false"
  76   | True           => "true"
  77   | integer        => _
  78   | real           => _
  79   | string         => "\"" _ "\""
  80   | var            => _
  81   | boolean        => _
  82   | binop          => "(" 2 1 3 ")"  // reorder the arguments
  83   | unaryop        => "(" _ _")"
  84   | add            => "+"
  85   | sub            => "-"
  86   | mul            => "*"
  87   | divide         => "/"
  88   | mod            => "mod"
  89   | logical_and    => "and"
  90   | logical_or     => "or"
  91   | eq             => "="
  92   | ne             => "<>"
  93   | gt             => ">"
  94   | lt             => "<"
  95   | ge             => ">="
  96   | le             => "<="
  97   | uminus         => "-"
  98   | logical_not    => "not"
  99   | assign_stmt    => _ ":=" _ ";"
 100   | while_stmt     => "while" _ "do" { _ } "end while;"
 101   | if_stmt        => "if" _ "then" { _ } "else" { _ } "endif;"
 102   | print_stmt     => "print" _ ";"
 103   | block_stmt     => "begin" { _ / _ } "end"
 104   | primitive_type => _
 105   | pointer_type   => _ "^"
 106   | array_type     => "array" bound "of" element
 107   | function_type  => arg "->" ret
 108   | decl           => "var" name ":" typ ";"
 109   | labeled_type   => _ ":" _
 110   | #[]            => ""
 111   | #[...]         => _ / _
 112   ;
 113
 114 /////////////////////////////////////////////////////////////////////////////
 115 //  Generate the interfaces to instantiated polymorphic datatypes.
 116 //  These are not strictly necessary since the instantiation is in the
 117 //  same file below.  However, in general the 'instantiate extern' declaration
 118 //  must be placed in the .h files for each instance of a polymorphic
 119 //  datatype.
 120 /////////////////////////////////////////////////////////////////////////////
 121 instantiate extern datatype
 122    List<Type>, List<Stmt>, List<LabeledType>, List<Decl>;
 123
 124 /////////////////////////////////////////////////////////////////////////////
 125 //  Now instantiate all the datatypes.
 126 /////////////////////////////////////////////////////////////////////////////
 127 instantiate datatype Exp, BOOL, BinOp, UnaryOp, Stmt, Type, Decl, LabeledType,
 128                      List<Type>, List<Stmt>, List<LabeledType>, List<Decl>;
 129
 130 /////////////////////////////////////////////////////////////////////////////
 131 //  Defines the interface of a rewrite class Simplify.
 132 //  All types that are referenced (directly or indirectly) should be
 133 //  declared in the interface.
 134 /////////////////////////////////////////////////////////////////////////////
 135 rewrite class Simplify
 136    ( Exp, BOOL, BinOp, UnaryOp, Stmt, Type, Decl, LabeledType,
 137      List<Decl>, List<Stmt>, List<Type>, List<LabeledType>
 138    )
 139 {
 140 public:
 141    Simplify() {}
 142    // Method to print an error message
 143    void error(const char message[]) { cerr << message << '\n'; }
 144 };
 145
 146 /////////////////////////////////////////////////////////////////////////////
 147 //  Now defines the rewrite rules.  These rules will be compiled into
 148 //  efficient pattern matching code by the translator.  A real life
 149 //  system will probably have many more rules than presented here.
 150 //  (A machine code generator usually needs a few hundred rules)
 151 //  Currently there are about 60 rules in this class.
 152 /////////////////////////////////////////////////////////////////////////////
 153 rewrite Simplify
 154 {
 155    // Type coercion rules from integer -> real
 156    binop(some_op, integer x, real y): binop(some_op,real(x),real(y))
 157 |  binop(some_op, real x, integer y): binop(some_op,real(x),real(y))
 158
 159    // Constant folding rules for integers and reals.
 160 |  binop(add,    integer x, integer y): integer(x + y)
 161 |  binop(sub,    integer x, integer y): integer(x - y)
 162 |  binop(mul,    integer x, integer y): integer(x * y)
 163 |  binop(divide, integer x, integer 0): { error("division by zero"); }
 164 |  binop(divide, integer x, integer y): integer(x / y)
 165 |  binop(mod,    integer x, integer 0): { error("modulo by zero"); }
 166 |  binop(mod,    integer x, integer y): integer(x % y)
 167 |  binop(add,    real x,    real y):    real(x + y)
 168 |  binop(sub,    real x,    real y):    real(x - y)
 169 |  binop(mul,    real x,    real y):    real(x * y)
 170 |  binop(divide, real x,    real 0.0):  { error("division by zero"); }
 171 |  binop(divide, real x,    real y):    real(x / y)
 172 |  unaryop(uminus, integer x):          integer(-x)
 173 |  unaryop(uminus, real    x):          real(-x)
 174
 175 // Constant folding rules for relational operators
 176 |  binop(eq,  integer x, integer y):    boolean((BOOL)(x == y))
 177 |  binop(ne,  integer x, integer y):    boolean((BOOL)(x != y))
 178 |  binop(gt,  integer x, integer y):    boolean((BOOL)(x > y))
 179 |  binop(lt,  integer x, integer y):    boolean((BOOL)(x < y))
 180 |  binop(ge,  integer x, integer y):    boolean((BOOL)(x >= y))
 181 |  binop(le,  integer x, integer y):    boolean((BOOL)(x <= y))
 182 |  binop(eq,  real x,    real y):       boolean((BOOL)(x == y))
 183 |  binop(ne,  real x,    real y):       boolean((BOOL)(x != y))
 184 |  binop(gt,  real x,    real y):       boolean((BOOL)(x > y))
 185 |  binop(lt,  real x,    real y):       boolean((BOOL)(x < y))
 186 |  binop(ge,  real x,    real y):       boolean((BOOL)(x >= y))
 187 |  binop(le,  real x,    real y):       boolean((BOOL)(x <= y))
 188
 189 // Constant folding rules for boolean operators
 190 |  binop(logical_and, boolean x, boolean y):  boolean((BOOL)(x && y))
 191 |  binop(logical_or,  boolean x, boolean y):  boolean((BOOL)(x || y))
 192 |  unaryop(logical_not, boolean x):           boolean((BOOL)(! x))
 193
 194 // Simple algebraic laws for integers
 195 |  binop(add, integer 0, x        ):  x
 196 |  binop(add, x,         integer 0):  x
 197 |  binop(sub, x,         integer 0):  x
 198 |  binop(mul, integer 0, x        ):  integer(0)
 199 |  binop(mul, x,         integer 0):  integer(0)
 200 |  binop(mul, integer 1, x        ):  x
 201 |  binop(mul, x,         integer 1):  x
 202 |  binop(divide, x,      integer 1):  x
 203
 204 // Simple algebraic laws for reals
 205 |  binop(add, real 0.0, x        ):  x
 206 |  binop(add, x,         real 0.0):  x
 207 |  binop(sub, x,         real 0.0):  x
 208 |  binop(mul, real 0.0, x        ):  real(0.0)
 209 |  binop(mul, x,         real 0.0):  real(0.0)
 210 |  binop(mul, real 1.0, x        ):  x
 211 |  binop(mul, x,         real 1.0):  x
 212 |  binop(divide, x,      real 1.0):  x
 213 // more ...
 214
 215 // Simple strength reduction (assume CSE will be applied)
 216 |  binop(mul, integer 2, x):  binop(add,x,x)
 217 |  binop(mul, x, integer 2):  binop(add,x,x)
 218 // more ...
 219
 220 // Simple boolean identities
 221 |  binop(logical_and, boolean False, _): boolean(False)
 222 |  binop(logical_and, boolean True, b):  b
 223 |  binop(logical_and, _, boolean False): boolean(False)
 224 |  binop(logical_and, b, boolean True):  b
 225 |  binop(logical_or,  boolean True, _):  boolean(True)
 226 |  binop(logical_or,  boolean False, b): b
 227 |  binop(logical_or,  _, boolean True):  boolean(True)
 228 |  binop(logical_or,  b, boolean False): b
 229 // more ...
 230
 231 // The following rules eliminate unreachable statements.
 232 |  if_stmt(boolean True, a, _):          a
 233 |  if_stmt(boolean False, _, b):         b
 234 |  #[while_stmt(boolean False, _) ... continuation]: continuation
 235 // more ...
 236
 237 };
 238
 239 /////////////////////////////////////////////////////////////////////////////
 240 //  The main program.
 241 //  We'll test it with a simple program.
 242 /////////////////////////////////////////////////////////////////////////////
 243 int main()
 244 {
 245    // Instantiate a rewriting object.
 246    Simplify simplify;
 247
 248    // The input is the following block:
 249    //
 250    //  var x : int;
 251    //  var y : int;
 252    //  var z : array [10 * 30] of int;
 253    //  begin
 254    //     x = 0 + y * 1;
 255    //     while (1 <> 1) y := y + 1;
 256    //     print (not false);
 257    //  end
 258    //
 259    Stmt prog =
 260       block_stmt( #[ decl("x", primitive_type("integer")),
 261                      decl("y", primitive_type("integer")),
 262                      decl("z", array_type(primitive_type("integer"),
 263                                   binop(mul,integer(10), integer(30))
 264                                          )
 265                          )
 266                   ],
 267                   #[
 268                    assign_stmt("x",
 269                       binop(add,integer(0),
 270                          binop(mul,var("y"),integer(1)))),
 271                    while_stmt(binop(ne, integer(1), integer(1)),
 272                               assign_stmt("y",
 273                                  binop(add,var("y"),integer(1)))),
 274                    print_stmt(unaryop(logical_not,boolean(False)))
 275                   ]
 276                 );
 277    cout << "Before:\n" << prog << "\n\n";
 278    simplify(prog);
 279    cout << "After:\n"  << prog << "\n";
 280    return 0;
 281 }