scala/ex_jvm.scala
author Christian Urban <urbanc@in.tum.de>
Thu, 10 Jan 2019 13:18:07 +0000
changeset 296 3fee65a40838
parent 228 e9ef4ada308b
permissions -rw-r--r--
updated to Isabelle 2018
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
225
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
// compiles Abacus programs directly to Javabyte code
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
import scala.sys.process._
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
import lib._
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
import abacus._
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
import recs._
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
import comp2._
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
def compile_aprog(p: AProg) : String = {
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
  def compile_inst(i: AInst, l: Int) : List[String] = {
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
    ("L" + l.toString + ":") :: (i match {
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
      case Inc(n) => List("iinc " + n.toString + " 1")
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
      case Dec(n, l) => List("iload " + n.toString, "ifeq L" + l.toString, "iinc " + n.toString + " -1")
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    16
      case Goto(l) => List("goto L" + l.toString)
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    17
    })
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
  }
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
  
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    20
  val code = for ((i, l) <- p.zipWithIndex) 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
    yield compile_inst(i, l).mkString("", "\n", "\n") 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
  code.mkString
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
}
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    25
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    26
def init_regs(ns: List[Int]) : String = {
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
  
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
  val code = for ((n, i) <- ns.zipWithIndex)
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
    yield List("bipush " + n.toString, "istore " + i.toString).mkString("", "\n", "\n") 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    30
  
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    31
  code.mkString
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
}
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
def print_result(l: Int, r: Int, class_name: String) : String = {
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    35
  List("L" + l.toString + ":", 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
       "iload " + r.toString,
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
       "invokestatic " + class_name + "/" + class_name + "/write(I)V").mkString("", "\n", "\n")
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
}
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
  
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
// compiler preludes
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
def beginning(class_name: String) : String = { 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
"\n.class public " + class_name + "." + class_name + """
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
.super java/lang/Object
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    44
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
.method public <init>()V
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
   aload_0
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    47
   invokenonvirtual java/lang/Object/<init>()V
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    48
   return
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
.end method
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
.method public static write(I)V 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
    .limit locals 5 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
    .limit stack 5 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    54
    iload 0 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    55
    getstatic java/lang/System/out Ljava/io/PrintStream; 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
    swap 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
    invokevirtual java/io/PrintStream/println(I)V 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
    return 
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
.end method
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    61
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
.method public static main([Ljava/lang/String;)V
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    63
   .limit locals 200
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    64
   .limit stack 200
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    65
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    66
""" }
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    67
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
val ending = """
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    70
   return
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    71
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    72
.end method
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    73
"""
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    74
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    75
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    76
def compile(f: Rec, ns: List[Int]) : Unit = {
228
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 227
diff changeset
    77
  val class_name = "Prog" + ns.mkString  // name of the class and program
225
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    78
  val (aprog, res, max) = compile_rec(f)
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    79
227
10d4d20c4e4b tuned scala examples
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 226
diff changeset
    80
  val init_code = init_regs(ns.padTo(max, 0))  // initialising registers with input data
225
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    81
  val main_code = compile_aprog(aprog.p) 
227
10d4d20c4e4b tuned scala examples
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 226
diff changeset
    82
  val end_code = print_result(aprog.p.length, res, class_name)
10d4d20c4e4b tuned scala examples
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 226
diff changeset
    83
  val code = beginning(class_name) + init_code + main_code + end_code + ending
225
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    84
  
227
10d4d20c4e4b tuned scala examples
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 226
diff changeset
    85
  val fw = new java.io.FileWriter(class_name + ".j") // temporary file
10d4d20c4e4b tuned scala examples
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 226
diff changeset
    86
  fw.write(code) 
10d4d20c4e4b tuned scala examples
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 226
diff changeset
    87
  fw.close()
225
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    89
  val _ = ("java -jar jvm/jasmin-2.4/jasmin.jar " + class_name + ".j").!!
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    90
  val start = System.nanoTime()
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    91
  val result = ("java " + class_name + "/" + class_name).!!
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    92
  val end = System.nanoTime()
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    93
  println("Result: " + result + "  Time: " + (end - start) / 1.0e9)
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    94
}
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    95
226
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 225
diff changeset
    96
print("Add(69, 30)   "); compile(Add, List(69, 30))
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 225
diff changeset
    97
print("Mult(13, 9)   "); compile(recs.Mult, List(13, 9))
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 225
diff changeset
    98
print("Power(3, 4)   "); compile(Power, List(3, 4))
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 225
diff changeset
    99
print("Strt:  ");  compile(Strt(2), List(2,3))
225
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   100
226
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 225
diff changeset
   101
println("FACTORIAL")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 225
diff changeset
   102
228
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 227
diff changeset
   103
for (i <- 7 to 9) {
226
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 225
diff changeset
   104
  println("Input:  " + i)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 225
diff changeset
   105
  compile(Fact, List(i))
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 225
diff changeset
   106
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 225
diff changeset
   107
228
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 227
diff changeset
   108
226
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 225
diff changeset
   109
println("PRIME TEST")
225
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   110
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   111
for (i <- 10 to 20) {
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   112
  println("Input:  " + i)
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   113
  compile(Prime, List(i))
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   114
}
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   115
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   116
0974c59e7029 added an abacus to javabyte code compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   117