Skip to content

Commit

Permalink
Initial commit
Browse files Browse the repository at this point in the history
  • Loading branch information
rymiel committed May 29, 2024
0 parents commit f884585
Show file tree
Hide file tree
Showing 13 changed files with 1,343 additions and 0 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
_build
2 changes: 2 additions & 0 deletions .ocamlformat
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
profile = default
version = 0.26.2
4 changes: 4 additions & 0 deletions bin/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
(executable
(public_name jvmilia_verify)
(name main)
(libraries jvmilia))
19 changes: 19 additions & 0 deletions bin/main.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
open Jvmilia.Verify
open Jvmilia.Testclasses
open Jvmilia.Basic

let test_loader (name : string) : jclass =
Printf.printf "\027[33m! bootstrap class loader is loading %S\027[0m\n" name;
match name with
| "java/lang/Object" -> java_lang_Object
| "java/lang/String" -> java_lang_String
| "test/One" -> test_One
| "test/Two" -> test_Two
| _ -> failwith (Printf.sprintf "test_loader can't load %S" name)

let () =
initialize_bootstrap_loader test_loader;
let cls = load_class Sys.argv.(1) bootstrap_loader in
let safe = classIsTypeSafe cls in
Printf.printf "Class %S is safe: %B\n" cls.name safe;
if safe then print_endline "\027[32;1mSUCCESS!!\027[0m"
17 changes: 17 additions & 0 deletions dune-project
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
(lang dune 3.15)

(name jvmilia)

(generate_opam_files true)

(source
(github rymiel/jvmilia))

(authors "Emilia Kond")

(license LICENSE)

(package
(name jvmilia)
(depends ocaml dune))

26 changes: 26 additions & 0 deletions jvmilia.opam
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
authors: ["Emilia Kond"]
license: "LICENSE"
homepage: "https://github.com/rymiel/jvmilia"
bug-reports: "https://github.com/rymiel/jvmilia/issues"
depends: [
"ocaml"
"dune" {>= "3.15"}
"odoc" {with-doc}
]
build: [
["dune" "subst"] {dev}
[
"dune"
"build"
"-p"
name
"-j"
jobs
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
]
dev-repo: "git+https://github.com/rymiel/jvmilia.git"
264 changes: 264 additions & 0 deletions lib/basic.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,264 @@
module StringMap = Map.Make (String)

type exception_handler = {
starti : int;
endi : int;
target : int;
class_name : string option;
}

type method_desc = { cls : string; name : string; desc : string }

type instrbody =
| Aload_0
| Aload_1
| Aload_2
| Aload_3
| Aload of int
| Invokespecial of method_desc
| Return
| Iconst_m1
| Iconst_0
| Iconst_1
| Iconst_2
| Iconst_3
| Iconst_4
| Iconst_5
| Istore_0
| Istore_1
| Istore_2
| Istore_3
| Istore of int
| Iload_0
| Iload_1
| Iload_2
| Iload_3
| Iload of int
| Iadd
| Ireturn
| If_acmpeq of int
| If_acmpne of int
| Goto of int

let string_of_instr (i : instrbody) : string =
let inner = function
| Aload i -> ("aload", string_of_int i)
| Aload_0 -> ("aload_0", "")
| Aload_1 -> ("aload_1", "")
| Aload_2 -> ("aload_2", "")
| Aload_3 -> ("aload_3", "")
| Invokespecial i ->
("invokespecial", Printf.sprintf "%s.%s %s" i.cls i.name i.desc)
| Return -> ("return", "")
| Iconst_m1 -> ("iconst_m1", "")
| Iconst_0 -> ("iconst_0", "")
| Iconst_1 -> ("iconst_1", "")
| Iconst_2 -> ("iconst_2", "")
| Iconst_3 -> ("iconst_3", "")
| Iconst_4 -> ("iconst_4", "")
| Iconst_5 -> ("iconst_5", "")
| Istore_0 -> ("istore_0", "")
| Istore_1 -> ("istore_1", "")
| Istore_2 -> ("istore_2", "")
| Istore_3 -> ("istore_3", "")
| Istore i -> ("istore", string_of_int i)
| Iload_0 -> ("iload_0", "")
| Iload_1 -> ("iload_1", "")
| Iload_2 -> ("iload_2", "")
| Iload_3 -> ("iload_3", "")
| Iload i -> ("iload", string_of_int i)
| Iadd -> ("iadd", "")
| Ireturn -> ("ireturn", "")
| If_acmpeq i -> ("if_acmpeq", string_of_int i)
| If_acmpne i -> ("if_acmpne", string_of_int i)
| Goto i -> ("goto", string_of_int i)
in
let mnemonic, args = inner i in
Printf.sprintf "%-13s %s" mnemonic args

type jinstruction = int * instrbody

type class_access_flags = {
is_public : bool;
is_final : bool;
is_super : bool;
is_interface : bool;
is_abstract : bool;
is_synthetic : bool;
is_annotation : bool;
is_enum : bool;
is_module : bool;
}

let class_access_flags_of_int (num : int32) : class_access_flags =
{
is_public = Int32.logand num 0x0001l <> 0l;
is_final = Int32.logand num 0x0010l <> 0l;
is_super = Int32.logand num 0x0020l <> 0l;
is_interface = Int32.logand num 0x0200l <> 0l;
is_abstract = Int32.logand num 0x0400l <> 0l;
is_synthetic = Int32.logand num 0x1000l <> 0l;
is_annotation = Int32.logand num 0x2000l <> 0l;
is_enum = Int32.logand num 0x4000l <> 0l;
is_module = Int32.logand num 0x8000l <> 0l;
}

type method_access_flags = {
is_public : bool;
is_private : bool;
is_protected : bool;
is_static : bool;
is_final : bool;
is_synchronized : bool;
is_bridge : bool;
is_varargs : bool;
is_native : bool;
is_abstract : bool;
is_strict : bool;
is_synthetic : bool;
}

let method_access_flags_of_int (num : int32) : method_access_flags =
{
is_public = Int32.logand num 0x0001l <> 0l;
is_private = Int32.logand num 0x0002l <> 0l;
is_protected = Int32.logand num 0x0004l <> 0l;
is_static = Int32.logand num 0x0008l <> 0l;
is_final = Int32.logand num 0x0010l <> 0l;
is_synchronized = Int32.logand num 0x0020l <> 0l;
is_bridge = Int32.logand num 0x0040l <> 0l;
is_varargs = Int32.logand num 0x0080l <> 0l;
is_native = Int32.logand num 0x0100l <> 0l;
is_abstract = Int32.logand num 0x0400l <> 0l;
is_strict = Int32.logand num 0x0800l <> 0l;
is_synthetic = Int32.logand num 0x1000l <> 0l;
}

type jloader = Bootstrap | UserDefined of string
type flags = { is_this_uninit : bool }

(** verification type *)
type vtype =
| Top
| OneWord
| Int
| Float
| Reference
| Uninitialized
| UninitializedThis
| UninitializedOffset of int
| TwoWord
| Long
| Double
| Class of string * jloader
| Array of arraytype
| Null
| Void (* unspecified in the spec *)

and arraytype = T of vtype | Byte | Char | Short | Boolean
and frame = { locals : vtype list; stack : vtype list; flags : flags }
and jstack_map = int * frame

and code_attribute = {
frame_size : int;
max_stack : int;
handlers : exception_handler list;
code : jinstruction list;
stack_map_desc : delta_frame list;
}

(* TODO: i dont think this is circular anymore, investigate *)
and jattribute = Code of code_attribute | Placeholder

and jmethod = {
name : string;
access_flags : method_access_flags;
desc : string;
attributes : jattribute list;
}

and jclass = {
name : string;
access_flags : class_access_flags;
superclass : string option;
superinterfaces : string list;
methods : jmethod list;
mutable loader : jloader option;
}

and frame_desc = Same | SameLocals1StackItem of vtype
and delta_frame = int * frame_desc

let empty_frame =
{ locals = []; stack = []; flags = { is_this_uninit = false } }

type bootstrap_loader = {
known : jclass StringMap.t ref;
load : string -> jclass;
}

let rec string_of_vtype (t : vtype) : string =
match t with
| Top -> "~top"
| OneWord -> "~oneword"
| Int -> "int"
| Float -> "float"
| Reference -> "~reference"
| Uninitialized -> "~uninitialized"
| UninitializedThis -> "uninitializedthis"
| UninitializedOffset i -> Printf.sprintf "uninitialized(%d)" i
| TwoWord -> "~twoword"
| Long -> "long"
| Double -> "double"
| Class (n, _) -> n
| Array b -> Printf.sprintf "%s[]" (string_of_arraytype b)
| Null -> "null"
| Void -> "void"

and string_of_arraytype (t : arraytype) : string =
match t with
| T v -> string_of_vtype v
| Byte -> "byte"
| Char -> "char"
| Short -> "short"
| Boolean -> "boolean"

let string_of_stack (stack : vtype list) : string =
let stack_s = List.map string_of_vtype stack in
Printf.sprintf "[%s]>" (String.concat ", " stack_s)

let string_of_frame (f : frame) : string =
let locals_s =
List.mapi (fun i s -> Printf.sprintf "%d=%s" i (string_of_vtype s)) f.locals
in
let stack = string_of_stack f.stack in
Printf.sprintf "{locals=[%s]; stack=%s}" (String.concat ", " locals_s) stack

type merged_code = Instruction of jinstruction | StackMap of jstack_map

type jenvironment = {
cls : jclass;
mth : jmethod;
return : vtype;
instructions : merged_code list;
max_stack : int;
exception_handlers : exception_handler list;
}

type vclass = string * jloader

let bootstrap_loader_ref : bootstrap_loader option ref = ref None

let initialize_bootstrap_loader (loader : string -> jclass) : unit =
match !bootstrap_loader_ref with
| Some _ -> failwith "Bootstrap loader has already been initialized"
| None ->
bootstrap_loader_ref :=
Some { known = ref StringMap.empty; load = loader }

let bootstrap_loader_impl () : bootstrap_loader =
match !bootstrap_loader_ref with
| Some loader -> loader
| None -> failwith "Bootstrap loader has not been initialized"

let bootstrap_loader = Bootstrap
Loading

0 comments on commit f884585

Please sign in to comment.