src/HOL/MicroJava/JVM/JVMListExample.thy
author kleing
Tue Feb 26 15:45:32 2002 +0100 (2002-02-26)
changeset 12951 a9fdcb71d252
parent 12911 704713ca07ea
child 12973 8040cce614e5
permissions -rw-r--r--
introduces SystemClasses and BVExample
berghofe@12442
     1
(*  Title:      HOL/MicroJava/JVM/JVMListExample.thy
berghofe@12442
     2
    ID:         $Id$
berghofe@12442
     3
    Author:     Stefan Berghofer
berghofe@12442
     4
*)
berghofe@12442
     5
kleing@12911
     6
header {* \isaheader{Example for generating executable code from JVM semantics} *}
berghofe@12442
     7
kleing@12951
     8
theory JVMListExample = SystemClasses + JVMExec:
berghofe@12442
     9
berghofe@12442
    10
consts
kleing@12951
    11
  list_nam :: cnam
kleing@12951
    12
  test_nam :: cnam
berghofe@12442
    13
  append_name :: mname
berghofe@12442
    14
  makelist_name :: mname
berghofe@12442
    15
  val_nam :: vnam
berghofe@12442
    16
  next_nam :: vnam
kleing@12951
    17
  test_name_loc :: loc_
berghofe@12442
    18
berghofe@12442
    19
constdefs
kleing@12951
    20
  list_name :: cname
kleing@12951
    21
  "list_name == Cname list_nam"
kleing@12951
    22
  
kleing@12951
    23
  test_name :: cname
kleing@12951
    24
  "test_name == Cname test_nam"
kleing@12951
    25
berghofe@12442
    26
  val_name :: vname
berghofe@12442
    27
  "val_name == VName val_nam"
berghofe@12442
    28
berghofe@12442
    29
  next_name :: vname
berghofe@12442
    30
  "next_name == VName next_nam"
berghofe@12442
    31
kleing@12951
    32
  append_ins :: bytecode
kleing@12951
    33
  "append_ins == 
berghofe@12442
    34
       [Load 0,
berghofe@12442
    35
        Getfield next_name list_name,
berghofe@12442
    36
        Dup,
berghofe@12442
    37
        LitPush Null,
berghofe@12442
    38
        Ifcmpeq 4,
kleing@12951
    39
        Load 1,       
kleing@12951
    40
        Invoke list_name append_name [Class list_name],
berghofe@12442
    41
        Return,
berghofe@12442
    42
        Pop,
berghofe@12442
    43
        Load 0,
berghofe@12442
    44
        Load 1,
berghofe@12442
    45
        Putfield next_name list_name,
berghofe@12442
    46
        LitPush Unit,
kleing@12951
    47
        Return]"
berghofe@12442
    48
kleing@12951
    49
  list_class :: "jvm_method class"
kleing@12951
    50
  "list_class ==
kleing@12951
    51
    (Object,
kleing@12951
    52
     [(val_name, PrimT Integer), (next_name, Class list_name)],
kleing@12951
    53
     [((append_name, [Class list_name]), PrimT Void,
kleing@12951
    54
        (3, 0, append_ins,[(1,2,8,Xcpt NullPointer)]))])"
kleing@12951
    55
kleing@12951
    56
  make_list_ins :: bytecode
kleing@12951
    57
  "make_list_ins ==
berghofe@12442
    58
       [New list_name,
berghofe@12442
    59
        Dup,
berghofe@12442
    60
        Store 0,
berghofe@12442
    61
        LitPush (Intg 1),
berghofe@12442
    62
        Putfield val_name list_name,
berghofe@12442
    63
        New list_name,
berghofe@12442
    64
        Dup,
berghofe@12442
    65
        Store 1,
berghofe@12442
    66
        LitPush (Intg 2),
berghofe@12442
    67
        Putfield val_name list_name,
berghofe@12442
    68
        New list_name,
berghofe@12442
    69
        Dup,
berghofe@12442
    70
        Store 2,
berghofe@12442
    71
        LitPush (Intg 3),
berghofe@12442
    72
        Putfield val_name list_name,
berghofe@12442
    73
        Load 0,
berghofe@12442
    74
        Load 1,
kleing@12951
    75
        Invoke list_name append_name [Class list_name],
berghofe@12442
    76
        Load 0,
berghofe@12442
    77
        Load 2,
kleing@12951
    78
        Invoke list_name append_name [Class list_name],
berghofe@12442
    79
        LitPush Unit,
kleing@12951
    80
        Return]"
kleing@12951
    81
kleing@12951
    82
  test_class :: "jvm_method class"
kleing@12951
    83
  "test_class ==
kleing@12951
    84
    (Object, [],
kleing@12951
    85
     [((makelist_name, []), PrimT Void, (3, 2, make_list_ins,[]))])"
berghofe@12442
    86
kleing@12951
    87
  E :: jvm_prog
kleing@12951
    88
  "E == SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
kleing@12951
    89
kleing@12951
    90
  start_heap :: aheap
kleing@12951
    91
  "start_heap == empty (XcptRef NullPointer \<mapsto> (Xcpt NullPointer, empty))
kleing@12951
    92
                       (XcptRef ClassCast \<mapsto> (Xcpt ClassCast, empty))
kleing@12951
    93
                       (XcptRef OutOfMemory \<mapsto> (Xcpt OutOfMemory, empty))
kleing@12951
    94
                       (Loc test_name_loc \<mapsto> (test_name, empty))"
berghofe@12442
    95
berghofe@12442
    96
  start_state :: jvm_state
berghofe@12442
    97
  "start_state ==
kleing@12951
    98
    (None, start_heap, [([], [Addr (Loc test_name_loc), arbitrary, arbitrary], test_name, (makelist_name, []), 0)])"
berghofe@12442
    99
berghofe@12442
   100
types_code
kleing@12951
   101
  cnam ("string")
berghofe@12442
   102
  vnam ("string")
berghofe@12442
   103
  mname ("string")
kleing@12522
   104
  loc_ ("int")
berghofe@12442
   105
berghofe@12442
   106
consts_code
kleing@12522
   107
  "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
berghofe@12442
   108
berghofe@12442
   109
  "wf" ("true?")
berghofe@12442
   110
berghofe@12442
   111
  "arbitrary" ("(raise ERROR)")
berghofe@12442
   112
  "arbitrary" :: "val" ("{* Unit *}")
kleing@12951
   113
  "arbitrary" :: "cname" ("Object")
berghofe@12442
   114
kleing@12951
   115
  "test_name_loc" ("0")
kleing@12951
   116
kleing@12951
   117
  "list_nam" ("\"list\"")
kleing@12951
   118
  "test_nam" ("\"test\"")
berghofe@12442
   119
  "append_name" ("\"append\"")
berghofe@12442
   120
  "makelist_name" ("\"makelist\"")
berghofe@12442
   121
  "val_nam" ("\"val\"")
berghofe@12442
   122
  "next_nam" ("\"next\"")
berghofe@12442
   123
berghofe@12442
   124
ML {*
kleing@12522
   125
fun new_addr p none loc hp =
kleing@12522
   126
  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
berghofe@12442
   127
  in nr 0 end;
berghofe@12442
   128
*}
berghofe@12442
   129
berghofe@12442
   130
subsection {* Single step execution *}
berghofe@12442
   131
kleing@12951
   132
generate_code 
kleing@12951
   133
  test = "exec (E, start_state)"
berghofe@12442
   134
berghofe@12442
   135
ML {* test *}
kleing@12951
   136
ML {* exec (E, the it) *}
kleing@12951
   137
ML {* exec (E, the it) *}
kleing@12951
   138
ML {* exec (E, the it) *}
kleing@12951
   139
ML {* exec (E, the it) *}
kleing@12951
   140
ML {* exec (E, the it) *}
kleing@12951
   141
ML {* exec (E, the it) *}
kleing@12951
   142
ML {* exec (E, the it) *}
kleing@12951
   143
ML {* exec (E, the it) *}
kleing@12951
   144
ML {* exec (E, the it) *}
kleing@12951
   145
ML {* exec (E, the it) *}
kleing@12951
   146
ML {* exec (E, the it) *}
kleing@12951
   147
ML {* exec (E, the it) *}
kleing@12951
   148
ML {* exec (E, the it) *}
kleing@12951
   149
ML {* exec (E, the it) *}
kleing@12951
   150
ML {* exec (E, the it) *}
kleing@12951
   151
ML {* exec (E, the it) *}
kleing@12951
   152
ML {* exec (E, the it) *}
kleing@12951
   153
ML {* exec (E, the it) *}
kleing@12951
   154
ML {* exec (E, the it) *}
kleing@12951
   155
ML {* exec (E, the it) *}
kleing@12951
   156
ML {* exec (E, the it) *}
kleing@12951
   157
ML {* exec (E, the it) *}
kleing@12951
   158
ML {* exec (E, the it) *}
kleing@12951
   159
ML {* exec (E, the it) *}
kleing@12951
   160
ML {* exec (E, the it) *}
kleing@12951
   161
ML {* exec (E, the it) *}
kleing@12951
   162
ML {* exec (E, the it) *}
kleing@12951
   163
ML {* exec (E, the it) *}
kleing@12951
   164
ML {* exec (E, the it) *}
kleing@12951
   165
ML {* exec (E, the it) *}
kleing@12951
   166
ML {* exec (E, the it) *}
kleing@12951
   167
ML {* exec (E, the it) *}
kleing@12951
   168
ML {* exec (E, the it) *}
kleing@12951
   169
ML {* exec (E, the it) *}
kleing@12951
   170
ML {* exec (E, the it) *}
kleing@12951
   171
ML {* exec (E, the it) *}
kleing@12951
   172
ML {* exec (E, the it) *}
kleing@12951
   173
ML {* exec (E, the it) *}
kleing@12951
   174
ML {* exec (E, the it) *}
kleing@12951
   175
ML {* exec (E, the it) *}
kleing@12951
   176
ML {* exec (E, the it) *}
kleing@12951
   177
ML {* exec (E, the it) *}
kleing@12951
   178
ML {* exec (E, the it) *}
kleing@12951
   179
ML {* exec (E, the it) *}
kleing@12951
   180
ML {* exec (E, the it) *}
kleing@12951
   181
ML {* exec (E, the it) *}
kleing@12951
   182
ML {* exec (E, the it) *}
kleing@12951
   183
ML {* exec (E, the it) *}
kleing@12951
   184
ML {* exec (E, the it) *}
kleing@12951
   185
ML {* exec (E, the it) *}
kleing@12951
   186
ML {* exec (E, the it) *}
kleing@12951
   187
ML {* exec (E, the it) *}
kleing@12951
   188
ML {* exec (E, the it) *}
berghofe@12442
   189
kleing@12522
   190
end