From 963ae07cf537219432e72249c51c931c966c011d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Wed, 3 May 2017 02:45:35 +0300 Subject: [PATCH 01/41] Rename identifier --- src/member.fun | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/member.fun b/src/member.fun index 5a82e29..2490ec9 100644 --- a/src/member.fun +++ b/src/member.fun @@ -34,7 +34,7 @@ functor Member(Flag : sig type t val compile : t -> Word.word end) = val (attrBytes, constPool) = List.foldl compileAttrs seed attributes val (nameIndex, constPool) = ConstPool.withUtf8 constPool name val (descIndex, constPool) = ConstPool.withUtf8 constPool (Descriptor.compile descriptor) - val methodBytes = Word8Vector.concat [ + val memberBytes = Word8Vector.concat [ u2 (Word.toInt (mask accessFlags)), u2 nameIndex, u2 descIndex, @@ -42,6 +42,6 @@ functor Member(Flag : sig type t val compile : t -> Word.word end) = attrBytes ] in - (methodBytes, constPool) + (memberBytes, constPool) end end From ccc7e57b5ea5d646a74d586085ede37e88b1c811 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Thu, 4 May 2017 00:43:54 +0300 Subject: [PATCH 02/41] Remove unused code --- src/labeled-instr.sml | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index a803eb7..4d701d9 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -226,17 +226,6 @@ structure LabeledInstr = val compare = String.compare end) - structure State = - struct - type t = { - constPool : ConstPool.t, - stackSize : int, - maxStack : int, - maxLocals : int, - bytes : Word8Vector.vector, - seenLabels : Instr.offset LabelMap.map - } - end fun compileList constPool instrs = let From 8f22adbb3a410afef321eaa0746a7ca60a918314 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Thu, 4 May 2017 00:48:30 +0300 Subject: [PATCH 03/41] Add Instr.toString and LabeledInstr.toString --- src/instr.sml | 206 ++++++++++++++++++++++++++++++++++++++++++ src/labeled-instr.sml | 5 + 2 files changed, 211 insertions(+) diff --git a/src/instr.sml b/src/instr.sml index 4aa6352..1443ac2 100644 --- a/src/instr.sml +++ b/src/instr.sml @@ -641,4 +641,210 @@ structure Instr = | breakpoint => (vec [0wxCA], 0, constPool) | impdep1 => (vec [0wxFE], 0, constPool) | impdep2 => (vec [0wxFF], 0, constPool) + + fun toString instr = + case instr of + nop => "nop" + | aconst_null => "aconst_null" + | 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" + | lconst_0 => "lconst_0" + | lconst_1 => "lconst_1" + | fconst_0 => "fconst_0" + | fconst_1 => "fconst_1" + | fconst_2 => "fconst_2" + | dconst_0 => "dconst_0" + | dconst_1 => "dconst_1" + | bipush word => "bipush" + | sipush short => "sipush" + | ldc const => "ldc" + | iload index => "iload" + | lload index => "lload" + | fload index => "fload" + | dload index => "dload" + | aload index => "aload" + | iload_0 => "iload_0" + | iload_1 => "iload_1" + | iload_2 => "iload_2" + | iload_3 => "iload_3" + | lload_0 => "lload_0" + | lload_1 => "lload_1" + | lload_2 => "lload_2" + | lload_3 => "lload_3" + | fload_0 => "fload_0" + | fload_1 => "fload_1" + | fload_2 => "fload_2" + | fload_3 => "fload_3" + | dload_0 => "dload_0" + | dload_1 => "dload_1" + | dload_2 => "dload_2" + | dload_3 => "dload_3" + | aload_0 => "aload_0" + | aload_1 => "aload_1" + | aload_2 => "aload_2" + | aload_3 => "aload_3" + | iaload => "iaload" + | laload => "laload" + | faload => "faload" + | daload => "daload" + | aaload => "aaload" + | baload => "baload" + | caload => "caload" + | saload => "saload" + | istore index => "istore" + | lstore index => "lstore" + | fstore index => "fstore" + | dstore index => "dstore" + | astore index => "astore" + | istore_0 => "istore_0" + | istore_1 => "istore_1" + | istore_2 => "istore_2" + | istore_3 => "istore_3" + | lstore_0 => "lstore_0" + | lstore_1 => "lstore_1" + | lstore_2 => "lstore_2" + | lstore_3 => "lstore_3" + | fstore_0 => "fstore_0" + | fstore_1 => "fstore_1" + | fstore_2 => "fstore_2" + | fstore_3 => "fstore_3" + | dstore_0 => "dstore_0" + | dstore_1 => "dstore_1" + | dstore_2 => "dstore_2" + | dstore_3 => "dstore_3" + | astore_0 => "astore_0" + | astore_1 => "astore_1" + | astore_2 => "astore_2" + | astore_3 => "astore_3" + | iastore => "iastore" + | lastore => "lastore" + | fastore => "fastore" + | dastore => "dastore" + | aastore => "aastore" + | bastore => "bastore" + | castore => "castore" + | sastore => "sastore" + | pop => "pop" + | pop2 => "pop2" + | dup => "dup" + | dup_x1 => "dup_x1" + | dup_x2 => "dup_x2" + | dup2 => "dup2" + | dup2_x1 => "dup2_x1" + | dup2_x2 => "dup2_x2" + | swap => "swap" + | iadd => "iadd" + | ladd => "ladd" + | fadd => "fadd" + | dadd => "dadd" + | isub => "isub" + | lsub => "lsub" + | fsub => "fsub" + | dsub => "dsub" + | imul => "imul" + | lmul => "lmul" + | fmul => "fmul" + | dmul => "dmul" + | idiv => "idiv" + | ldiv => "ldiv" + | fdiv => "fdiv" + | ddiv => "ddiv" + | irem => "irem" + | lrem => "lrem" + | frem => "frem" + | drem => "drem" + | ineg => "ineg" + | lneg => "lneg" + | fneg => "fneg" + | dneg => "dneg" + | ishl => "ishl" + | lshl => "lshl" + | ishr => "ishr" + | lshr => "lshr" + | iushr => "iushr" + | lushr => "lushr" + | iand => "iand" + | land => "land" + | ior => "ior" + | lor => "lor" + | ixor => "ixor" + | lxor => "lxor" + | iinc (index, inc) => "iinc" + | i2l => "i2l" + | i2f => "i2f" + | i2d => "i2d" + | l2i => "l2i" + | l2f => "l2f" + | l2d => "l2d" + | f2i => "f2i" + | f2l => "f2l" + | f2d => "f2d" + | d2i => "d2i" + | d2l => "d2l" + | d2f => "d2f" + | i2b => "i2b" + | i2c => "i2c" + | i2s => "i2s" + | lcmp => "lcmp" + | fcmpl => "fcmpl" + | fcmpg => "fcmpg" + | dcmpl => "dcmpl" + | dcmpg => "dcmpg" + | ifeq offset => "ifeq" + | ifne offset => "ifne" + | iflt offset => "iflt" + | ifge offset => "ifge" + | ifgt offset => "ifgt" + | ifle offset => "ifle" + | if_icmpeq offset => "if_icmpeq" + | if_icmpne offset => "if_icmpne" + | if_icmplt offset => "if_icmplt" + | if_icmpge offset => "if_icmpge" + | if_icmpgt offset => "if_icmpgt" + | if_icmple offset => "if_icmple" + | if_acmpeq offset => "if_acmpeq" + | if_acmpne offset => "if_acmpne" + | getstatic _ => "getstatic" + | putstatic _ => "putstatic" + | getfield _ => "getfield" + | putfield _ => "putfield" + | invokevirtual _ => "invokevirtual" + | invokespecial _ => "invokespecial" + | invokestatic _ => "invokestatic" + | invokeinterface _ => "invokeinterface" + | invokedynamic _ => "invokedynamic" + | new className => "new" + | newarray _ => "newarray" + | anewarray index => "anewarray" + | arraylength => "arraylength" + | athrow => "athrow" + | checkcast index => "checkcast" + | instanceof index => "instanceof" + | monitorenter => "monitorenter" + | monitorexit => "monitorexit" + | goto offset => "goto" + | jsr offset => "jsr" + | ret index => "ret" + | tableswitch => "tableswitch" + | lookupswitch => "lookupswitch" + | ireturn => "ireturn" + | lreturn => "lreturn" + | freturn => "freturn" + | dreturn => "dreturn" + | areturn => "areturn" + | return => "return" + | wide => "wide" + | multianewarray _ => "multianewarray" + | ifnull offset => "ifnull" + | ifnonnull offset => "ifnonnull" + | goto_w offset => "goto_w" + | jsr_w offset => "jsr_w" + | breakpoint => "breakpoint" + | impdep1 => "impdep1" + | impdep2 => "impdep2" end diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index 4d701d9..ce1e549 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -226,6 +226,11 @@ structure LabeledInstr = val compare = String.compare end) + fun toString instr = + case instr of + INSTR instr => "INSTR " ^ Instr.toString instr + | LABEL label => "LABEL " ^ label + | GOTO { label, instr, ... } => "GOTO (" ^ label ^ ", " ^ Instr.toString (instr 0) ^ ")" fun compileList constPool instrs = let From a13d48b27ff0d6f3bf83793ae1dd7b92a4618b2e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Thu, 4 May 2017 01:25:22 +0300 Subject: [PATCH 04/41] First take at generating the StackMapTable attribute; incomplete and buggy --- lib.cm | 8 + src/attr.sml | 54 +++++- src/class.sml | 2 +- src/java.sml | 46 +++++ src/labeled-instr.sml | 56 ++++-- src/main.sml | 64 ++++++- src/stack-map/frame.dot | 41 +++++ src/stack-map/frame.pdf | Bin 0 -> 26668 bytes src/stack-map/frame.sml | 53 ++++++ src/stack-map/stack-lang.sml | 267 ++++++++++++++++++++++++++++ src/stack-map/stack-map.sml | 112 ++++++++++++ src/stack-map/verification-type.sml | 87 +++++++++ src/stack-map/verifier.sig | 4 + src/stack-map/verifier.sml | 251 ++++++++++++++++++++++++++ 14 files changed, 1018 insertions(+), 27 deletions(-) create mode 100644 src/java.sml create mode 100644 src/stack-map/frame.dot create mode 100644 src/stack-map/frame.pdf create mode 100644 src/stack-map/frame.sml create mode 100644 src/stack-map/stack-lang.sml create mode 100644 src/stack-map/stack-map.sml create mode 100644 src/stack-map/verification-type.sml create mode 100644 src/stack-map/verifier.sig create mode 100644 src/stack-map/verifier.sml diff --git a/lib.cm b/lib.cm index 657e0d4..8ead60a 100644 --- a/lib.cm +++ b/lib.cm @@ -13,6 +13,7 @@ is src/descriptor.sml src/field.sml src/instr.sml + src/java.sml src/labeled-instr.sml src/main.sml src/member.fun @@ -23,3 +24,10 @@ is src/text.sml src/util.sig src/util.sml + + src/stack-map/frame.sml + src/stack-map/stack-lang.sml + src/stack-map/stack-map.sml + src/stack-map/verification-type.sml + src/stack-map/verifier.sig + src/stack-map/verifier.sml diff --git a/src/attr.sml b/src/attr.sml index 467a4b2..b7ee006 100644 --- a/src/attr.sml +++ b/src/attr.sml @@ -26,7 +26,7 @@ structure Attr = exceptionTable : ExceptionInfo.t list, attributes : t list } - | StackMapTable + | StackMapTable of (Instr.offset * Instr.t) list | Exceptions of ClassName.t list | BootstrapMethods of ConstPool.bootstrap_method list | InnerClasses @@ -58,6 +58,7 @@ structure Attr = | Signature typeSignature => compileSignature constPool typeSignature | SourceFile value => compileSourceFile constPool value | BootstrapMethods methods => compileBootstrapMethods constPool methods + | StackMapTable instrs => compileStackMapTable constPool instrs | attribute => raise Fail "not implemented" (* https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.3 *) @@ -67,12 +68,35 @@ structure Attr = (u2 0, constPool) (* TODO: add exceptions *) fun compileAttributes constPool attributes = - (u2 0, constPool) (* TODO: add attributes *) + let + fun fold (attr, { bytes, length, constPool }) = + let + val (attrBytes, constPool) = compile constPool attr + in + { + bytes = Word8Vector.concat [bytes, attrBytes], + length = length + 1, + constPool = constPool + } + end + + val seed = { + bytes = vec [], + length = 0, + constPool = constPool + } + + val { bytes, length, constPool } = List.foldl fold seed attributes + val bytes = Word8Vector.concat [u2 length, bytes] + in + (bytes, constPool) + end val (attrNameIndex, constPool) = ConstPool.withUtf8 constPool "Code" - val (instrBytes, constPool) = compileInstructions constPool code + (* TODO: generate and add StackMapTable only if version >= 50 *) + val (instrBytes, constPool, stackMapTable) = compileInstructions constPool code val (exceptionBytes, constPool) = compileExceptions constPool exceptionTable - val (attributeBytes, constPool) = compileAttributes constPool attributes + val (attributeBytes, constPool) = compileAttributes constPool (stackMapTable :: attributes) val attributeLength = Word8Vector.length instrBytes + Word8Vector.length exceptionBytes + @@ -91,7 +115,7 @@ structure Attr = and compileInstructions constPool code = let val result = LabeledInstr.compileList constPool code - + val stackMapTable = StackMapTable (#offsetedInstrs result) val bytes = Word8Vector.concat [ u2 (#maxStack result), u2 (#maxLocals result), @@ -99,7 +123,7 @@ structure Attr = (#bytes result) ] in - (bytes, (#constPool result)) + (bytes, #constPool result, stackMapTable) end and compileConstantValue constPool value = @@ -216,6 +240,22 @@ structure Attr = (bytes, constPool) end + and compileStackMapTable constPool instrs = + let + val frames = StackLang.compileCompact (StackLang.interpret (Verifier.verify instrs)) + val (stackMapBytes, constPool) = StackMap.compileFrames constPool frames + val (attrIndex, constPool) = ConstPool.withUtf8 constPool "StackMapTable" + val attributeLength = 2 + Word8Vector.length stackMapBytes + val bytes = Word8Vector.concat [ + u2 attrIndex, + u4 attributeLength, + u2 (List.length frames), + stackMapBytes + ] + in + (bytes, constPool) + end + fun minimumVersion attr = case attr of Custom => { major = 45, minor = 3 } @@ -237,7 +277,7 @@ structure Attr = | RuntimeVisibleAnnotations => { major = 49, minor = 0 } | RuntimeInvisibleAnnotations => { major = 49, minor = 0 } | LocalVariableTypeTable => { major = 49, minor = 0 } - | StackMapTable => { major = 50, minor = 0 } + | StackMapTable _ => { major = 50, minor = 0 } | BootstrapMethods _ => { major = 51, minor = 0 } | MethodParameters => { major = 52, minor = 0 } | RuntimeVisibleTypeAnnotations => { major = 52, minor = 0 } diff --git a/src/class.sml b/src/class.sml index 22fe803..302356b 100644 --- a/src/class.sml +++ b/src/class.sml @@ -50,7 +50,7 @@ structure Class = val constPool = ConstPool.empty val magic = vec [0wxCA, 0wxFE, 0wxBA, 0wxBE] val minorVersion = u2 0 - val majorVersion = u2 49 + val majorVersion = u2 52 val (thisClassIndex, constPool) = ConstPool.withClass constPool thisClass val (superClassIndex, constPool) = ConstPool.withClass constPool superClass diff --git a/src/java.sml b/src/java.sml new file mode 100644 index 0000000..283a349 --- /dev/null +++ b/src/java.sml @@ -0,0 +1,46 @@ +structure java = + let + structure D = Descriptor + val class = ClassName.fromString + in + struct + structure lang = + struct + structure Integer = + struct + val toString = { + class = class "java/lang/Integer", + name = "toString", + descriptor = D.Method { + params = [D.Int], + return = D.Type (D.Object (class "java/lang/String")) + } + } + end + + structure System = + struct + val out = { + class = class "java/lang/System", + name = "out", + descriptor = D.Field (D.Object (class "java/io/PrintStream")) + } + end + end + + structure io = + struct + structure PrintStream = + struct + val println = { + class = class "java/io/PrintStream", + name = "println", + descriptor = D.Method { + params = [D.Object (class "java/lang/String")], + return = D.Void + } + } + end + end + end + end diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index ce1e549..bd2685d 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -235,23 +235,26 @@ structure LabeledInstr = fun compileList constPool instrs = let fun traverse [] state = state - | traverse (instr :: rest) (state as { offset, constPool, stackSize, maxStack, maxLocals, bytes, seenLabels }) = + | traverse (instr :: rest) (state as { index, offset, constPool, stackSize, maxStack, maxLocals, bytes, seenLabels, offsetedInstrs }) = case instr of GOTO { label, instr, byteCount } => let in case LabelMap.find (seenLabels, label) of - SOME labelOffset => + SOME (labelOffset, labelIndex) => let + val offsetedInstr = instr labelIndex val instr = instr (labelOffset - offset) val (opcodes, stackDiff, constPool) = Instr.compile constPool instr in traverse rest { + index = index + 1, offset = offset + Word8Vector.length opcodes, constPool = constPool, stackSize = stackSize + stackDiff, maxStack = Int.max (maxStack, stackSize + stackDiff), maxLocals = maxLocals, bytes = Word8Vector.concat [bytes, opcodes], - seenLabels = seenLabels + seenLabels = seenLabels, + offsetedInstrs = (offset, offsetedInstr) :: offsetedInstrs } end | NONE => @@ -262,68 +265,94 @@ structure LabeledInstr = * has been found. *) val result = traverse rest { + index = index + 1, offset = offset + byteCount, constPool = constPool, stackSize = stackSize, maxStack = maxStack, maxLocals = maxLocals, bytes = Util.vec [], - seenLabels = seenLabels + seenLabels = seenLabels, + offsetedInstrs = [] } in case LabelMap.find (#seenLabels result, label) of NONE => raise Fail ("undefined label: " ^ label) - | SOME labelOffset => + | SOME (labelOffset, labelIndex) => let + (* + * We're doing a kind of a dirty thing here. We're + * misusing the instruction's offset field by putting + * the *index* of the target instruction. The index + * as it appears in our instruction list, not in the + * final byte stream. + *) + val offsetedInstr = instr labelIndex val instr = instr (labelOffset - offset) val (opcodes, stackDiff, constPool) = Instr.compile (#constPool result) instr in { - offset = #offset result, + index = index + 1, + offset = #offset result, (* TODO: check this is correct *) constPool = constPool, stackSize = stackSize + stackDiff, - maxStack = Int.max (maxStack, stackSize + stackDiff), + maxStack = Int.max (#maxStack result, stackSize + stackDiff), maxLocals = #maxLocals result, - bytes = Word8Vector.concat [bytes, opcodes, #bytes result], - seenLabels = #seenLabels result + seenLabels = #seenLabels result, + bytes = Word8Vector.concat [ + bytes, + opcodes, + #bytes result + ], + offsetedInstrs = List.concat [ + #offsetedInstrs result, + [(offset, offsetedInstr)], + offsetedInstrs + ] } end end end | LABEL label => traverse rest { + index = index, offset = offset, constPool = constPool, stackSize = stackSize, maxStack = maxStack, maxLocals = maxLocals, bytes = bytes, - seenLabels = LabelMap.insert (seenLabels, label, offset) + seenLabels = LabelMap.insert (seenLabels, label, (offset, index)), + offsetedInstrs = offsetedInstrs } | INSTR instr => let val (opcodes, stackDiff, constPool) = Instr.compile constPool instr in traverse rest { + index = index + 1, offset = offset + Word8Vector.length opcodes, constPool = constPool, stackSize = stackSize + stackDiff, maxStack = Int.max (maxStack, stackSize + stackDiff), maxLocals = maxLocals, bytes = Word8Vector.concat [bytes, opcodes], - seenLabels = seenLabels + seenLabels = seenLabels, + offsetedInstrs = (offset, instr) :: offsetedInstrs } end val seed = { + index = 0, offset = 0, constPool = constPool, stackSize = 0, maxStack = 0, maxLocals = 10, (* TODO: compute maxLocals *) bytes = Util.vec [], - seenLabels = LabelMap.empty + seenLabels = LabelMap.empty, + offsetedInstrs = [] } val result = traverse instrs seed @@ -332,7 +361,8 @@ structure LabeledInstr = bytes = #bytes result, maxStack = #maxStack result, maxLocals = #maxLocals result, - constPool = #constPool result + constPool = #constPool result, + offsetedInstrs = List.rev (#offsetedInstrs result) } end end diff --git a/src/main.sml b/src/main.sml index 7c0fc25..440a03f 100644 --- a/src/main.sml +++ b/src/main.sml @@ -154,16 +154,16 @@ structure Main = code = let open Instr in [ aload_0, arraylength, - iconst_1, + iconst_0, if_icmpne "else", - getstatic (symbol "java/lang/System" "out" "Ljava/io/PrintStream;"), + getstatic java.lang.System.out, ldc (Const.String "T"), - invokevirtual (symbol "java/io/PrintStream" "println" "(Ljava/lang/String;)V"), + invokevirtual java.io.PrintStream.println, goto "return", label "else", - getstatic (symbol "java/lang/System" "out" "Ljava/io/PrintStream;"), + getstatic java.lang.System.out, ldc (Const.String "F"), - invokevirtual (symbol "java/io/PrintStream" "println" "(Ljava/lang/String;)V"), + invokevirtual java.io.PrintStream.println, label "return", return ] end @@ -171,6 +171,44 @@ structure Main = ] } + val factorial = Method.from { + name = "main", + accessFlags = [Method.Flag.PUBLIC, Method.Flag.STATIC], + descriptor = Descriptor.Method { + return = Descriptor.Void, + params = [ + Descriptor.Array (Descriptor.Object (ClassName.fromString "java/lang/String")) + ] + }, + attributes = [ + Attr.Code { + exceptionTable = [], + attributes = [], + code = let open Instr in [ + iconst_5, + istore_1, + iconst_1, + istore_2, + label "enter-while", + iload_1, + ifle "exit-while", + iload_2, + iload_1, + imul, + istore_2, + iinc (0w1, Word8.fromInt ~1), + goto "enter-while", + label "exit-while", + getstatic java.lang.System.out, + iload_2, + invokestatic java.lang.Integer.toString, + invokevirtual java.io.PrintStream.println, + return + ] end + } + ] + } + val class = Class.from { accessFlags = [Class.Flag.PUBLIC], thisClass = ClassName.fromString "Main", @@ -188,7 +226,7 @@ structure Main = } ], (* methods = [main, printString, bootstrap] *) - methods = [withBranch] + methods = [factorial] } val trim = @@ -216,4 +254,18 @@ structure Main = in print (output ^ "\n") end + + fun stackMap () = + let + val { attributes = [Attr.Code { code, ... }], ... } = factorial + val { offsetedInstrs, ... } = Instr.compileList ConstPool.empty code + in + StackLang.compileCompact + ( + StackLang.interpret + ( + Verifier.verify offsetedInstrs + ) + ) + end end diff --git a/src/stack-map/frame.dot b/src/stack-map/frame.dot new file mode 100644 index 0000000..0ac215a --- /dev/null +++ b/src/stack-map/frame.dot @@ -0,0 +1,41 @@ +digraph { + rankdir = LR + + node [ + shape = circle + fontname = courier + ] + + node [group = chop] + Chop1 + Chop2 + Chop3 + + node [group = same] + Same + Full + + node [group = append] + Append1 + Append2 + Append3 + + Same -> Same [label = "α ≣ β"] + Same -> Full [label = "α ≢ β"] + + Same -> Chop1 [label = "(α, ⊤)"] + Chop1 -> Chop2 [label = "(α, ⊤)"] + Chop2 -> Chop3 [label = "(α, ⊤)"] + + Chop1 -> Full [label = "∀ α, β"] + Chop2 -> Full [label = "∀ α, β"] + Chop3 -> Full [label = "∀ α, β"] + + Same -> Append1 [label = "(⊤, β)"] + Append1 -> Append2 [label = "(⊤, β)"] + Append2 -> Append3 [label = "(⊤, β)"] + + Append1 -> Full [label = "∀ α, β"] + Append2 -> Full [label = "∀ α, β"] + Append3 -> Full [label = "∀ α, β"] +} diff --git a/src/stack-map/frame.pdf b/src/stack-map/frame.pdf new file mode 100644 index 0000000000000000000000000000000000000000..8248c4562dc7cb4da717807281f811ec411955dc GIT binary patch literal 26668 zcmd3OWpo_7nys1bn3-c{hM1X|89QcXJ7!4C%*+%+%#1NJ+c7gU^K+7ud+xk@=FR+k zt5>V4w$!ChQmtNlZ%IWeFDy#SNXHCA`hELi`>^mbYy5jJ3=1Ixp^c$A3^z9+y)?ku z#L<+H^$k)aq!%@_bOhMH9W4zU0m1+y8)E<=FE5OPqdmaD3dR+W zDjKM8yBkW8YLpp{Lc^)8vefF^V7Vnr zA?ETX&Us`NTSmIYMpiyyx{KO(GXXN;`!N!?8_YUr-Ag&)LJDVqh@P2msgiUB1ZIlK zx_Q)!0__VuPnIi2Nj)@)k*ONIx)C3f8HVcRdPiq9O)|EkN@r%f!4a?;%Frx$T9Ya= zGjN?fAL`vMPj>Zq8|ruV`F3pNHhlMcm$L0gu!mMwgl1{c?2}`MHVS6eh!T>in~P!T z$nLo3Qu>fhcK0N)ZxE=k&@rnau^mDxE^s*3yCfbhH)B7^&Zp0- zA#7?QU4Dhgu!cW!foLNb8|`ahuZ;9UpzXC|(%Zl_Uu+~&A5QF|L!y(aT;hDJs@Vx@ zVoHod=B%Et{g~6b_^@DkDEx8GX-s&nUdkLF)ToQ_{V>OCT2&(b;gRQ&-A+Bnbn~P zwDH@ByD=6kWO`96^APc#Y>|&@n z>lOmPw^}wrih94UUS2Nl`*ycT-9Z@z8k?x4erNRInNt?eG~G=DNuc4Er$orgQY5kY zWI^b(!7SOQ$kg$fUjS+X>Zdq!JFUMwrdb ztFqQjHbF>`S&yr3tTT02B=_2vCo1r0(lJBdZ|{9)&U<}D*NC| zI+Px1wGj6t`T_Rk5hVw9xxPtuZ{86^N_k2HyS@Q5+nXv~aq);o5DQJxm|QBzQjkxG z&^CgdhbiJG2^0+DGjI}O?7UMdtuaN!w8%|w4g24OSLZC*fnNM7e_G_ex@%Mc!1a zW&6bZjWoyyC(>YqFEos2+XNaChEUUUR4#XulE~07odx~{83vgYB-t#cX(-$%SHNO9 zXji~<3)Ov~rBb^EA_}Kwq8&?bqNbKrCnkNN|-mW+i5Tt)+U_@Ud(*s1focGya`#UXrhuBCU@EfkkBv2N%D@EtVM__F7?1qXppe27|y1MqsfL(MM zYDO%d`b~z4j^2F)0VzeSz)*u#Di#=18hM6YQUqIXNmL3+TQhJ1r8&h*u2b;EX%8@H zK$zt8UAf{q6J1D|B(4wj{0DNmFcz@5iLikYKn&aFXs10fR4|zxHxzZblq(IA#|D{n z;3fxmCsCl1HIlc7!X_fF0t~arQ)q~0iRmELR`cYv!zfM7h7^wrOO$eL7^PKQQ_H3& z)nUs!QQy$p7Mpy6u0XaGF`e8=&bbof!CnLd&UxlFqWmZ>h1GMA$dkhl2C2%)F&~x{ zNvFSiF~si&D#uD*g-AZ1*qi$u)xpOTpP0UUxaO*nIQ9N?zi(hBB>)t9>YIZteuDv8 zqTpPe`H2`PP}-=qQGMTeU(jr1|8d(-wu3{xGFG0e%o4%1YV8MV9xBvPE2h{Txhrla z##w~0t0+Y4u$N3XMRPjnjFXwazf@iHPK~vu?obQ){#x-oNteYUkLg<;M=ww95uP@z%GjNGTlCJkm_NVh94f~QdUoei?Spc~`$URi$s8dw zH=o9JoVKCZXLL+t^VkI}6@`1w#PQHFhc`%$3W+8_V4_Ox56+o|)U5RP#zQ4r;W23r z%h|3?MQJ=J8>Woxc^YW78x4bj@E}KtE%TVZTp&ij69DBStcfh)Wj4?I0q$#+Ow3e! zB^*8ovo2%@@~)D4#EWV2-HzZ?(Rmhf4g}n8fr6S0g2{ca{Y+j=8^MZN^5;vo9dsd- zEW!4UkMDt0z9+hu6HRxQGR0rf5&=~lW9Fl>!lJK>W1WDoA37#7mdmf&@P4}6Z-4zU z=3)a|XDdLqwN%b@6Gay>n3BX7-%pr&MLXIH?cT@q!SYKT;*B)m8qr%F0J@(Qe9Uct zn;tgu3GRJuAQJ3~V@J_DegnWH^fH2?Mt*T63r+1BW3hT9qqDS_4=~mh$3v=4#MRnj zP~>62<1C1puXbZotmF#&xCg>l?r?gql@-vaO@E;)KCgpsllo5h*J_l_G7@(nt z$P5_MBo1VfA- zg=OfpZNK@f<&j0501nMLhHN6GIJlQR=Xx80%fneV@)9|e|80{ga!K!3M;{%GtC2Gu49X8qw4j|2x>JbI zNQ)6H0q!T+rK`sE>wb>69}KuXD!id&-Sw~>aigqLz01XS3FIOvslw1xHIv1!(uxI9 zuT6(nF;~am!Sps&-}pJb9xP`ce%0mDibb=K#xoi-K^nM$bWM z18@K=fd3OA9!eV8xkp$V#6f_qNirm^qbJ04=QlH*7;Jb!B=3)u1UZ%BG`M3go{KvnxdqbKE=~N*y%u-AQ?F2CTVgjcnKX? zk{1_!5xJInxApt45Ky{3&%(0oxOukrIt(PS98{$x5;e2l?FzhipjV^V5Y#0uqn%;g z+(FID1&EJ@127?wrwBTSbPPU{cPF9vv_PlKLmCU3VOCo*GOr+v0$qs4BJ`KDI35>Pf++mH z8-lJnYl|9xNWWCN6D@*GcWDzf?h~pdq;n_Y(s|Zgw$&7?{6&3f4v<6+0n4>gG)j(n zWzg8Be@xA|9fA&Vzc2xKZImN$a7ke}rQp*30K5@~IUZQNTD4;8W~=%{1n`fWFv2n` zT3#8!=j>`G`ChS$*;eT}uqAuHEwq9x5TClOJD`&WPwQdc4(_wCMmF0%A^*!W$z;Kc zi&p9QXz(c5cqVGU=*;fr>m-@N!BN4TQ|@?PpJsnD%4a{+xs;}E{O)w_oSXRDHCegy z8x#Z&Y5{%@#mNFK=M-E42q$I}$Sg zruB*d2OB4QBY*=T+iyU~#@g{M-+}O_6nNwPG5}*U13?>CLM?_jfSsM4kcER$2j-3X z|5eY=-~Evc^7b}HN&rVft+&dAMG5JZ0j`dOI)wB>HkLN_O11_@0K%WjLdb!Ukp0)~ zd3oOy#aoTPU}a@iLPn;aI1IhAG9w|!uOe@!OoW_&PMHZAf5!0^n6ffEA>;2L-|q5v zJdA%j4gE#W<~%-F~R>?-=rtFC@U?Xe;#XPZyiS_ zCM3PWc84aM+fec2YrDk-`lAm zEV8{EW&wR##(KGu^4zDfy0BY6w_tMWIoAXv|KtbO<){wq!;-CzdUDvQjf^t%{T2ih z5g0)oxMTg}M=-HFVUX#kR-WYKBJtkpn-e-8rPJ%B$fS}^O zbGFzcgx+(SW&pVsm~4fB1xpwfAk8J2ZSVDed^oRGx;JE`j_a0L|Kch=c2xrx!GPgY zVUr*NOsZj(Y#M!BhI@RhF}q`W-@dSl@1^w2)9?PMa!z(MmLU+9p|NUt^p(C99q5Kc zGZnA8EnWqv#tMRed;P22DIw4WI8e<>+9iIFrEbjk4LEYx(4!+u2jEN#I_f?4$4oz) z!S*1|+vK5>M^&x@3_joY5@^f-k?n%Q0x99)VK{`uG2`c3#MjLZPP37LZkn{r4vh1_ zJr#w$IOu?2)8;^KU-c+DW0(N%nRRbWHgZTTuXGDkQztzj&p=N31_{W18y+B`_n;)! zeC{Bghgyh?F#T;Ure)C;4v|dmFS`!}u-YNk>(T9`-h-f(iB~j>k?~(;)5pgu3+=K+=IZ#1+ zgo2|GWBBjK$%-(k{7bThG(fnL5>r$Ks*C`1|TJYOc}t>1J(H~RC3`$ ziFFOF3A>`DL1J_)u1hwc^CHxDVXWhv0nr5Nb;UyQ_d|hBh^j;3oC^y^sgnRB5m`hN z=YbT9q(mX);WUPeN84?ILVV6PNWw(##oGL=5w>oqYA|ak$uN^-l%y(+vBUNek=gg& zFW+$HTY)fg^N_yS7lRpq~1@>vT9X{6y3SKZNT@v-^GRgIbyd_@>o*F`PLk#mVGB;>yG=IK$kcrJ z0r#fz-~T?2znsgA9Y*b))ws(WMhq zxth6Ly&Oh$b|L4yn_6U*!RZn)65#_fO7qhz%KA-XHDhoVJEmkTrL4_;Ih9Kq8ec_c zvpBoC`#(Lz3DA69$5NJ?pfU8^898^AZ|M;F_p=0FP7i7L^ zR6Sa-yi;3NOuOpbe(cGWqEoqy-YnZZc7t$3{7Cl52+8x=^>Zu2?YyHiMRS1X4ASA= zdc){>*d`>o2l=-tiNe)%jZw-`_|aTgIE*ulXEG`W4bUsSKI7qmBsi? z&BKRbnYr*?=kHeEm*;sFo*N#i-$}iT77Oi*D~#R69)s2Wl31Y@tyWPVb8C2Nep<-; zfj5{poEN3dxvkWb{?6bTr9+)VYDkLu~6Erfo6IgdA zaA&h00sW*NiS{%)h~Sfub09Y~E1VA6g99cV4a--uBew<>S1(r=Fj_+qVWIEM;*tH6 z{bHfv=u+q|q61<*A~Rw#A|4`%B2tO!G#b@gqG6h0gath41UP6OB+mB5x0B0KpEr*- zU^Y+an6(qCkAB$KZWj-Yl}G7yYS>ZX;}GDjBEANrbQNz)mtW~Mx@?2Z#WsI_jM?p_ z-VHz3xdS{!gCz!31xyGhe%A>$k|>uzlh_226R2Hts?xjg-71cYip!;BE}keJF$<`< ztC8^M$z>2~8Z?_ZQ9;S!pNN*GaM1YJoD}gQeJvhFl1l2Y0b6Ze zwPGR$$Q)D{M%uaBO4+g=!W+08c=TfZ$m-%`(&qdU^wi0EVu4T=I9sm0*eL6w)7i9s z-F6shMQA0ya5f}56b`^ywGLUCR>)GQY|}TbKHcdRY!p;jZ>1g8La^+yM6*0z{#adR zzL-d?J8^9|v=Oo)N4gYqxT@i)cE3D)6L8#`f0O^{vgQosvb4P4bg7W8;#~Wx zmG=~IIA{+fFFq=6i+BI6yhWLSRgb~a`q%EU!<>Vrb`x(sZ{cI{^XM_LK(YM3u1KdD zuIV}UBKA18uJD-NZ<}^~HqUF8F1VSZXuo}`{d7= zH+AEhA)48RoFJ5eYd{Rj)H7V!R;qpxPY&{No4xhzu z&PdQZ@-o}6J+*4xx2=9o*er`^1NYp0(0Qa^xoPs;j(APS0S$$CIH7Cvc-39v+4o#| zo`5WVr^`3&&hc#eY;?4lLk=THl~KZ1_B?Yp_p!M3>L_bYf2{h8Nn}ui5dCZXeT7^% z_*n56wP=m#fmoT?SlE5ovirBIp0lB_#Hr1|cFLE!+xUsnOfQ$mRujX4?`IYhhsk`B zD@ARb53@H`yT*H4Q!Zww1%)9irEPpSzR%f@Mpu2&`$uwja`Bnrd@i4$pDtX z{kw~P>mykMt2epwADwAwVDdIjOux$r{!(eQY^PX1S$x2AC!jh3K5j4wucBe`TD`xQQirA&&QLj>}+yElL(cTHntoF<~;OuLh1G9byuCYT3*z zdkVm$lf@#l^_=bj&|(Cbm{5(a-ljQ3j`G|-zP6u!+MRDc`O&Ho_vJBwO!e#j;spJb zoNX$i{bKJMLkMfSaVU?pTB;thncgNXZ+pShs>5+o!g_YGUZ~@{^}MtrYFUI}yR~9E z38mIvgfL||s0y@j)qgDa6xDgeC=ab){>JFC`ZWV*d8MBI_LE(7)9X#!accNW=XOck zW<+|ky%Y0X57)_$v_pE2A_BCSRfKyL12mUVkXEwqEJV_Rp_grnHrZoBdX3X9E4+{I z_vt1-Ki-1&UXN7&=p5o}WKwj@+T*lVw|{?Dq8w7?ScTjA6gxzZj+fMs>#fJ*r2ZuU zGg}9xAOIKXWA52|n4#}9(dYu}IeH2kV#AiL>Qp;lwuD1P9CfF}p1%01j#Iu`6v%nX zpoCUD|M)_&znqg1to+zy4c__jtIrE)k z=R1WO$_)cKb}H2%=yo)}Th=N~`O!4D+R6w%EzR?moQuZ6^j6+?^dH-P#M}nwUnnqG z1-sqMF(CUf8iyjf>&H zbIWM0j-wl^I5+JRO7-FsxV^4D&Rva8B^+W0 zP%mWPX{niN_TSDWwwyC$HmG?hji_<=e)3k5r%LHr%pD#Af!+}|@x22L9O|ekua+Fn zs|369E7RxWfRpu6TBC7A(*~+@8cw;DVR|H?FB~)*+}Ccr&VfNX2oH2O%3g6*c1@Oq zmSc1M0!7;=jz>y1PIvH~xDwkE*rQXx7LFSs1C-vs-p2}W>J=|A($`GKDAu~*&{(V4 z)G9d0FG0}D9)k5qgOb)6t3RH0RPczlu$HZT?YeG=)#X;Fp4pf(m?gk7AMG+@)%9X- z;k3fKL9ER@0vtp^DS9V0L)?j1Nok6>x&2=5ww@%E3Y}y(2o%jBG0pp~aA6`9`-Vhu zpy=aVc?JAFHj+uNSDB~ZNUE`Iz?UP@_tI|If#&*6)l>dG%j!$v|D0@io?*yWSqGdi z6YHELaT4P;PFC9HIq~A1?PKmvb?zaEx-c~PPvC`}=sQB@a$zq2g7js#iO}!F4+m99 zw~0njxHVBD(f#{KxPu(=X|L)ct4%)ha2+iej3Ib9&sTS6;N2Wm{)YM%-Y#`a%!-(}sgpK~;0Ra`M66T77NP}g)PL1C zQXp8-0vMc}VYwJnIs^)Ck{h0eN{ZtE+Q%;HQT17bMhvs(1&L zG#lRcL1sa0s9N9O+_c{!sU~Y(uLncHC*Elu-VuB_s}l3d2e|SbE=XS|iaurw$O^=% zubfW^v?{(f++}wTFgn$mfAnhM8Aev$Efy-eKRyG{jjzxehbsu2zgov4f6pz)CSq+^ z|50!K@?9Oys`KWe^{2&fo91&X_O|0+pvO}EGE^pmm~ld5(xJHueuNTx(cCRJPek{qr`O)4 zP$t2{)A;UZUcRgQUr@lh7^W8wOB}Oi()mn{5qGXk5-)e?UhO-aRN^`J)M9Q7gL4^^ zM*PTK@kzoeYgmP!>VB2-yGMP4im_`1gu;bP+?{t%U=>{N}wNGGxQtC z9tWcNIZ%TGh`o+qel*GF(It!o2@V_*4D+hAlAx50eauNFUHLl5OMv?r*tqaXmWBbz zso6(KC;1aRN`*uwDGviRZJoj%M7@t!CFCb)TyXMEtTSYecULs)IxqylC@J`3P>Wb< zSS!|FQ)E?T3fD=QDQSRP^{MCIA^4-Lp>n|Lf@AnxAd{1&4-JdXm&|-=Y=Wdy4jE7K zA|J2L(j*P|(ZY|Y08ax)Rp-nUAjJ7q(ifK_1ysyo%@hH5#5b4ImIX3mr(@z5sAR#0 z|H1`B02-Tt?g;al*H>0|tN@)_y2F*Nx0*2{{M<6k#E2Vba{+U#_a_v*>dy!2`AxB0 zAWg_UuV}aed}a?gKhQ@|gfxtqf(C*|ALt15bBEm-7$!u8PrYyWJ@_~NP~LW^ODQZE zx$Lv)hAySBM8g);&3sJy9#_g?S#0c6;qPL!3#4zb>rX4AYZIDA8cA)x=Y9ES3O&c z$&%nwq&C-8ZOqKpF4<4`oOjE`GI5)pb~flgD`pqm+~S6xYay4PY`avn+X-Agl-5_{)6A-q$aq|CD^7Go&W2J0PZ8*HG0V zQ4lrm)9)V*J!;vkx+F%SXFC6ym)(Y5I6{mXc@Oz3BEpxsAHsVl1bVl_6oG#HoIg2iE=bHx^Y<_wJ2I1ETxhRx;YZzZ5J3u0ifD! z9sij4;|mTZ$@}x>Xu54O47S-sw7Ia=))j4KQ`HAK^|$cUut3eR2mP2!->%MFet1fv zd0a?1b*w43E)Q+pxy(z6QFx8dp85FA7H;CFUr3jr%ddmRB zJQyYnhtKC6bhCH&$xrefCeULCku5Gau=pyY7tkgoCho3+FRNu9oM>A?s&*xgRKGaC z3$2F6)o{J@kYokD?rP}pFAJ5Q>99NgBDuyw;7HrSK#gtyi;1xASE>#%SM$W;1=o`1kqJY zzo*EgDEKPtHhI?#Wxft1I44DFW$c{CJ9X`8P3p--mZMA8FT=E{FzkAfqbtg43|A78 zlp|3{l{+SsZ%_5oqx__#;R5%*uQwdGyPq-aACoDx@(n%d%x^grG4%>=g+GJ>`9Vk& zJRe!9*kktO@G$r7Gwma$p9DlO{P<4JY2D5qj9#NhNjA@q`u6#khsUi_>pxMmH1kG{ zdf|rVH%BA|W-5`WiPYtmUP6*r;{nUYnICTG-tV1wKs;9COhZVeGaA6L)$DMdZ6isE zsgIXjT~-<{vxVetFvW{RdI$to8TaIo!cVA;H)BRuQJqKNqm^F9D#S<2TB4?c7L4CM zq#PL97x$5y*e%7j4O$)?=1+YRZY(JkY%EE^PlX}6ZhbyIpTODP6+Nd6HJ!fBi)f|3 zngo%Iy{z1aDb}AIWxq;#a4}A!no^dXAAKxVFCPV;*_V8O%=p7d_?mMNmveM12i?gV z_|_(+Qlq*`!$Ef|DIfdeHtVnw{N)97MPhM!OgQQTamG%F1=wq&wywzXHhb!jDl zCK(sl?lUMsT5&oSNpe9-r2><7dFTo(n!y~DY+0IvapSjgbT7#?h(;<&oPp$X5ACuC zB46ihx0A`42u`QY@z&rUmY{l}MhVlREJcCp)fB!X0KM&9%9Y4&@Jv7fbjDr2F^odTbBiB$QcOHM$F!v7rWg$Ur`w%NJ3_e9dIOZCa3f z>QGO?(Hg%1`p}Tr@>R$=>|z6bQX9=9E$*pljGPh5b4~mhqR&V!rfTq;@{w6UCz2(- zaPDXcOou_bNBwA7Y?}jF1Fa$p>NaB{*Oz2C(d`m3H{D3=8TnW-fGk0*7;9OHSm^;{ z+njPA%lSDCudGjwq4BvL2?jZTkJ~K=FqN!N2ujulSP_RV&Km?RZ^y$QZ!e0P2_;X( z(dYvsYo1sfF{pSCJebE8F$YGGzL>x!TT?L;I>3SPfC5~?o4&$;l|5O#nv7ANDdKbB zodkq-!aJp^Cg!6^A_`I-Qht7i3VU~8)HZOZe5$04QZiR5dO9szomm|7nkBog!X}dU z0!qCN@T~nlVxp)H;@+uRNq`GM-a%=L-U34h6t7ld)#N|t6qT>Ft`do=TIEQs(G*X! zESX?UDpenouQf1PX1xCkcBi}aOzaZlr=7zFJBP$_+|C&9eT`3p2dM@x-HeR^>gqbBqN zRhPT@JRTAw62oIFW-mE6R@1Y@?Hq$K76!{|_?UTdd3lSR{^`u~|CkuHTr{Kdf*iy% zpRsu%WX+xqDB;JW%)k0yLyD^sbFpH@XR7U|Fj5}T1B z^{osA%kU(P-{nXy6Gvr#O0C!#eluZT7c09=mhr*mSwMu8p2fjjb@9^+(iRtL^AK&vnF>sBwM_debWfqM< zUt=JqW>|5!TGjY*HSqw|r+P0s$F0KY@)r`!|H}&p&q3BUiQ$|gR$`mw>Lg0 zY9shT+*GLE2guV29$~r&0UIm;LSD|1WHPQ5i`Q5oKy+Gb?}t?JvLnxB2_GZwsWURXwfHYn zosfm?ZK~$Css6L=|1#AX+27jpZ>~Di?|GcRUG-nUpXUB?)&E-B^~Y6bWny~^;(v10 zTh(EeQPomjY*gA^;~YU@h}CDz1fqg=NWT!H&WD5K_y{)}K{SJ-ibL^2m5M^Unbw4t zmZHQmlJzD_lQ9pNPGHL!A#ak6k})%KoeVcMCAWP1Oi~?d=i)3jVjWk0Uy_oPw7C#l zZ8A2SfAZS$`nvqOvZ3nq+T_7SnGy7bys?$NGU#f^87Z&GGfOXIFu{?yds@Xp^;UHI z4u*L1X2!)v8!aA1DY(H*C*3!qNP12{syXY+;8!q5O*Na>pdw2y(3DRudXEh}jQIAS zZ1lTbz1-hbIm%_#GaqCwfq$@)S$%l1!@3`6{HU|rz;}t9ywadi@cexZkXLIALLh{z zF|mV~>}})j4_9gKtX-(Od|p9~OjXX1Dw62U;L<2Nrt@R_U@ zR1}aY@`TiGyA~uu@Oc!oplgXiW-K1X&}(53SyN-C5!bmWeqaWq8R8bCHSubtMfr^2u&c~)f`i)g?y42 zpkztT+WDz|h1pFo*7lo3(j190D|B^gK;i=KU{G>mY;~Yob)aqCS+1plLmfjD?H0i3 zieaYv>3!>KIn4}g<{Yfe46NKVtkz+m%yn0Zd#5h_S80rbd|0K)Kn5J{=t_12IglP7 zo;I=hX2>S$J{TQCr=;imd_%@L4XU7p2>DW!t!(*2Si@`K8=!4W%#SR>oD@F&Y_VE} zI2yjP?3EzPFKR?;2tj4=dFO_-P9dtj3BW{`aK-IR>q{Y2I4f!2 zVFG^SgG>H0UMu%$wpQrLE8p6yKs~a)U4=Yyo8L`v$(P~qvfI*3TwCoc;0wyB;CFlz z|9OOKU`~NymxN#`ZTirWa;J?A(}EB6_;$XBdAwzOLxN60>c@kKyQ*#PN9~Nrh`wp# z;3G@r41``>@1v>Gp*k?~bVJ*TT4cN8C^B)%wRqOL1>QS5B)b(fcBBDDS>#wvl45Ct z(Mth-q$|i4-_)hi{lOn+V{ldZVjQ3&6{`kHkYWW6;Xl~)Om&{Yneo^ScNtg&CO4@V zG?T$A=c|&c{us1auHSoVnmiqCor%vrvQghq@rqej3Ski)Ib)?@P84@>7n?6UGK%yF z@XSFXFy?xkp2|5qw$7xl70{U9g0Gh2UN*pN0uA|!#pf#+4QgvDpKxGD0ZDZWRcj7r z*Pu8!v7tYdaA3`qV@)UQo2vCbWs#!MksX7*q`5V>5#DC(yy3IMcxO+N+@e$Baqp)Q zaPUZC`VRTqN?5!WLp0T_O}Z~CSNvG+SsR88$~l*ApF=~|8ML+YQg!r_(-j<~rk8S3 z6TJbWktvzMDVe_as-!Qgdmk*?mWzyrGC!?l6;7?6b8)9PJP(fgmMa5H^GV?O&hkD+ zq4Ey3SG7vz`pRxgh!twNb*v`@B_3|J8SoY*Cvq)yJC08s;PFzpGzkrDZ{tIvU(MI) zSn#lK|FC;M_d}Jz~$UTMImw9$#rHBl#7%&v91`j?dAp+#x#3)(5YULyHh*@gS4qLz8Q zce9hLQFytsB^5$ylJxRP?Osn(G)$YcS*rsh0y|9_%h#J1Vpu6^aG*1ru=E6X{fI^Pt-|vpM3Z3exa$&c!k0}=FVD4Bhd+y z%_cyo+K#_fkEbL<(K{H8aT0909oUNKdJ5u)EEhv&tD~Q8VW@g3-vlNzGqn_O(B_fn z4VGA1_>e%2-kIm8C_Zz-Zh`K{Udhe((YwUC2j-g&k z+37o@_Ph5iy#8Z5u=i|UeBNKYS1QNm4YVzu%I)T_lHEM=cqWmszF0=IFVtohBa)HGK2Fsm-nXBV?Iz!{`Sw?J)=rt&#~&S*?W4A1cDLtYLt z_}4U*O3AgfzNN1S6+EFD)Uzg7msLQA23qrk9!Yq@9wB(W+!49qm5B?BN4U*CY=bXf zZa7W0hPA17*Qz*@E%>#9(AR!6(v_zkZaZi5^xeT{mx z5lYEkwar|&fj5Ca#TJEsHES@h!G;a1$4N|4l-Vu-o~kY|+G!r=8sL)Ry*t28>&P(JwVh&Uz&z0$MVJsMYxNQ-_fFl`HgJup?x zRLE&vEwwQnc139xtE5CGBP}agqk%#Ob#C{K5xsiAbnQH4>x#qtIVNUX4NfBh9QJ}` z0m+B>j5Sa%I;*60K`gq)4mipBB5u9$04KwKTB&V);Hx6I$`&VSq>$o@9akPhbM6AH zSK{J&Y@F1G)uKxeM_nMBdLy4LiDP>ym`f@AeCI6cz4PYFG)rO8Ys1U5dE6q=G<5ZB zH(y!~1k;S2b%jY>>qw>rV0<>-DU?0=l$2KdTh!*|#9ih27Uw?6KwMTy!IL{%E8G_= zlRDREuCayiSe@+jbG(R%bc1Bo2Ua@ULbY{J-oQ%>PRmBgknXZP%Lk5Y>T{{l%e}cU zm_!YnJ-At_DsS?T@?b9+7;czi0WJWVb?I1XWf@SR@Ax+{6C|E_re~fQGM{tj) zBF*!scNxPQh*JJ{BNDyL8waL!JFDO2ZMvWGWRmY|>B-OycXSitEiBmF1_{Bit8uJHBkTrTjH|{-=xEaMvew zMtG*So?80UR62xHpdW!_gwIqxTC;@dfMAaHW7lpE+*4QX(NVWPPE`|@btO4ja{tDN zLiOD2h~35-%-F_=31g{Ylbat2(@RStiPYGAROlKNsw|p)R7E9*U%T9~bPNQ(jaa8f zEL!72={jK#cCBddw{vuokP+rv$@&=}Vq` z0H6#qf>y1D_Wq>p$JuFIn;b(1taRbm@E$srTy~O?m2QT7)z$6jqcr8V@eI*~%NJ(Q z7&mt_jpC6H>8ZMGl%x~ABYM-7ck2L$7=&ShwB@HrGdY`A$XWcx4-E6ogxy}J1)*Ql zgUK-$O>TpTU(wx=YMT(aq<)0A)gkQrVGNvZ z8(5D)cE(1j^kq_bkaMoZEe)7xQxj$<&7dqzkZ%t@H06@|`E|P8}8QMQy^{9F zcPLmH@$gF7Yc+dt&F$7+T|=DQ!&0V5Ed7J7|Fb@jne}bS*pcKW|9VHjpOt!V>ilmx&;0Llo{f=_kd>9~zl!#M*s{a) z*Os0CNw?}mwOW5CL=5oAFdUMy>vGl%K-F=K34NlF#RuyCA^3sbG#s|w(}x3t5*(cQ z@>}U`jUknVIpSkBa5#5LP{S+5PmOX zW0{uj{eeIvf{>eDgoP=%!ipjJc!SXMAXr5|QB!z?!l$Ls;EIm|QD{83bdS8pyVB33 zytiMXZ~!^a#m4^Ktk|KJrlQ#?qNRr_uq3x*AAIaS#ORc&%$dz_M_7%#egLP{Yf-Dh zaj;gpl@Cn-$vA5(!8F8DA7l5Tu@(D=!Tz)1is|3>dj0!*8~z^ae|A0oafpAp9&h9H z)BE|kknsN})8o%pu|H2X)4wlW{bPFkwUG2*rUxs-&({1;FRf6AbyVt0elaDIpw z1jbp^mcZZ(ARVf+ysTubqHUbtF$g0uh-Sg&CF|?cW%M}4XWG7Aj!y9hMLqrZ;XZ)-ZE;f)V@_w8 zoG~Hto}#ZDqJcdt(|L10G|ahDJy$yM%}iE4z&3+iE4J1jc&4nNG;iPy^$#MX%nQ7K zR9Xh1GklVx%jO#qslg774Vr*m3Uk8i+v5;T!(Yz{ofmpG7}qtT@bLzr`gWds_C~to zVxt#zn{&2nXM##mUBhtqeq`#Zr@Vf9wP=7;bdO5F0_Zf{x!lzY zq^?EvcJ;@hiWJ&+ELzU&S|^ruU(M>~Q)o-=X_f40IU5r&7rmIS4CK05HIPt-c+UbWJFUEb`);stk}3=t;9y* zyYHlX5aq;kaI?1QP9f6z)U-Jwf}?}G_{cw5hLo|6q-5y?3BQ-BzH8%yN$4c-4Wmto z;zn8ljXhr}jpJ%Ljkv4%#XkCO!{=+jbB{&wkkY}D+u+w9YVqa-s>muIzw9gI6R)?l z246a%nSFNNKdp)=bvSvy3R4QL&;WUC6}BxD`k{1aXd}8OpLn zGNz7*R$KPAv6}R5wBMqm=;lisrSOYtTvhSPb}x3GAp~b|FgsY5VTPX0&ig`ZeKZ*v zEt1Kc*lU)+m`oz8G9 z1nQkST7U1?`4!#D+Jdlm<<_N-a1X&km*^7#+z3vPU}&9iy%0j>C!uLN#G^ARdnm5? zDwU=mZ2>7bs#!ZI;zc?n_2oM|7*4fnfj>HQKd-W{@k62sK_Abk++a%vz#wOQX+c%; z1hsY?$Iktx$a6Bum|{&K$G&yWpO3D?z#xC(+vQWJjnUlxe=55QsHnQGjjyi~1A=r) zNhmb|GlP^UDFV`s(jg@hLw86@BaL)OhqS^FO1C1Nf`l|8;D5mv{Y3x&{r*|7Sa+{; z?mc(!efFIFto>{V`G}?~ykAO_aecj`8BQP+M<9f=-YI|3Fl9UBR;tDlEl`#>F_E)> zJGX&|BYkC}FDhe2)1ds)vZDl6ew-qK`d}}U)k_5@iIpvr8pUMW2hRl89!|T`YiI6X z%$}IILjG~rZvT0EZTrD>97o-5kKiLJ=ariIhch1WdpGEU%!%uFK5o{}w{xMLytx`a z&ym&dpmsmjqn8fH0+$eDvx^^U9hx(x+1h%~QIPuA+YIw9jIIdtEx1yj$U#U$yQwgKpM#^{e4qRcFZ)j>I~)N$ z&T+y5W~9U)Klt#v)VqyE&MIFbWD`ae`rS5@S*cxbyFvT1OizhLyg*Syr z)HdZo9IZiDszGcH?yi!B7~>wp49d-5S-hXlrT-JMKH2O-KKQOP>-N^woNqRHZ{xj!zr_gEN&`C;$IRDe4XWvxV|U=aL7Q>yCQU~ zL4wYxu5%-*(I#(^EEB;RK>h9fkj-Jgu*Mg;BVO}`iAJX#wgd;RP2OxY+|EHe87o7$aC`CMw2ceC#APB< z7wa2L zu#m@MF<|euU`zy_Ls%VzlLd}h0#PO(%BHWyYdyzHtgO=ZP}!1N(>Y0q#6lL2SKl9f38bWM_q67sfxZ97H?L?O`CB0a92;`0ZM;Er&8O-IqJ6~+UB?A zeKlBa^IButYvARu8rp$1U|N{eM3XT)=SgEJl-hliQAFR+vPtZ})(4?k zY$DQEHK>dpAP7kB6cOOQ?HXqqtl45DCviACL&ZBK7XlGlfnuk!E|k-xPVq=DUvf_4 z)zFO`pd^2=yyiJwPsVtEoIr-cWDZ9qC;)BuaYqM^AQE6)w+@k3jtEE71&yqiR zshWt{Gt9rJiZx}VtUpXbMx>Sq`$o&hPq=HWjAFM$&7#OZybq|lnad##R*W~jttw2b z8KvvwqNeSP{cQy|=6)a*Ou)ZFv)iiqo18COgQRa>y_|2BR^XN|uB>=Rzlg8V!8Zfc zye$Phfhqog^TMn&Ql)tqRDb{T)fw3U;s;b+(`b9Vqlniu^W?@<7M8m+N6b^2X5_Q^ zZyunH5)d)^3K1fDxYiL@*Ci#z6o}Hy9`}h?v{d9zPk)Iqo!5HtEP2PIv$iachr4Fp zRC!EWj8N=5wY4?4mg)Wcw#*Il( zsMk4>+n1OOBqTxf$n9g%*=0cnG6{6A6a-(Gsw?Rz=?Lq1m?9`HfI0WqhfNe6p+pQs z0~onIO(`XRmHN=3|s*=VK$7Vrt$e#63&k=Vat# z`w+(4_1ZuRDrV6fts@mSs6->~T35fz7vH^&KxDMzu`7?gn|#4(gBpDtvNB%TFg}(2 zxx?J#p&nQ0!FKn1PJ1y^i=<9Cz4)8bdA1x~xZ0@@ z%Q{l`o|!Y|Cg`Cs5uL*#cD|43nc{HF(x1Juy_oO@ws@QSXr-F^0Nj~w#*I0GTgF^Q zr;Zp=E^{%)e||`8j|L`LGlySnZ^EarAod9X~m(?0PBQMg+QtH7K7Os#;?yQXGAGPqC{NyJ$u+R)XvFc z*eE(ZS9k2RtVPWCSgu!T@g~h~y$Q(6 zA5WdV9;}(m)}d1RYQccFxw-UGw8LIXS(rVAh6ZiD(W<5&e{tR?AF|4oa0fND?2>n# zG(LlTb^|>7xp^R^E`=6^6EAHHZ=r)dN>WY+K2f`9lpIR-Rn=`ek$XQ`-?M&53bl@m zz@6Hrs&3rK?W!*#fV?Glp$aDN4fp*LNXB)|Vr_MCbk_9K3iiZ~5aWh%#~+gQQ+gi^ z4*$`a<)p{S{~MVRy(_DxEXyWrWo2fd;9#z6X$J5=kJI&^Sw7JJ<$KM=PiO}A55?{$ ziSk!y2H^PpsI));#R@#UFyI%A^Pe2WlY5-5_n&+l_D^-kzh&53Po+)KU|gSFL7(XU z=1KImQm8M~fG+T;rwr4|jES7`1G0;uvT*sCOln{yDqL{=s_Sa9(;D>iE^&uD1@nS= zBahh|x*#N9xB9uEXU>ny4M}MzSWxeVgQV87Fyx^aN5XA!{g?b$sKlIE%PaLEyh2S= zpZEvf7B%k$gZ6Rp6mZyO%2q{NRqE(I2V8NIa*5exlyf6Wb`nVu5h)v%U{=*kgU6O7 zhrP*^+pw0ytveiEDtLt)V;0TRkLn2xkfd)@POR4DD-oT(x>Rw$fSnWnB_>?sPGq@j zPLkX-Z|JUg3xQNZE^S$eo#F2eaH6MU-9fp3Aaf^HI@RaDp*4Rt`yb#M7*Hz00Rt$X zFfbfR#|sDluO%w*W8&tq*Bo;|IgTr6ewL`v@o>X&{wYxb+d^_hlAG_3hlNP1kPr!UQFaT+bkr z6Mo8oTAx)~eiMkfJ#85gY-xv(2rTVzU2~ds~HiTx6GA&as`9Aj@vkq9CmK#@P*xA?TqDW zyEIh8D}94nIZCBy?iPyP{9(puM3>AqHS<9BB^d{jb}9S6V_vx%sM6mjbe}_$FJ8Zi zeo^Jc9brai629B*DDO~76;__#sCE?C;4vdodrryK6C8^qA;RXMCuCqH6pZ@D-Jm6w z_-w}HV9Zs(P1x;8EPR-NHuElRiItvlg43O4c(hd*$@|j&-8NR;^OjS}+1Egd4?vW6 z@b4FyF8K(K$YmU8^Onbcev`IIU7^;aT zbtTjyvp}e_*i2K4ir^L6x6q0P>t+S^RaXz0EGI!j`<_MNtiQ)97c>*kdz$LD$q7%r zC4&_|eq@`ej_WsbnaVHi5`OyyEb)Z#s#oW&9$mFPG+pW_(upihdmQyd-C-oeI=l%R znqMg{ap+;wN&%g0fM2@1+G{nrE+|O<<^FhJed{0g@hQX(2O~~#$dm3 z1w(s}6iZ%DQ3i{`xzp}Rrwy)TUI_ncMDq$s^QK@hS0?6J_%~Y|_4>VReZ>4|=6EV8 z#|8eW8AS-XB&7>sFwT{!JZsjo5t>ee0|LZd z4k+(2GoP0mAj~8FcVa#mDEs>vp@Av?5uxG7A@+L_ArPT|^74V8{v#^$Ab{$^pJjw# zZs79xtN?sn1LS;w~vv;AsW}e!5g)|yIkgovLdLVbu-BGz z`%K$ft30wiN@LjV{I;^+xQ8jp31nSQ-_^cN^LU=45Nolkj^DD7or?psXuR;H{to4> zYRWg8lW%jI+iz7ztXzgzzFsbxsPe0>%e7H^>6VbOnsi@X=}JJTgZ!sKkSVF(b`F1N zwzlGx5Ea498oRuZ&U-=7A`&|j13FS|^tljOhJxO#h8}SZ$p?EKvH4tzn%;k}BI`3{ zKv~IdDP@oC#T7&XU8t05&<`;`s7ljFFF$r%Smo*#%U|6wE<7R^Murc%A{B8NA_j#? z{BmOb@8ULNRO^M~=L+tTvlJ6Gx8Z3_%Z)H*a+QFoy&z9B{M5&MgEZKY*^W6V$+8kY zIm_ArX;t(#c~4Ze*=!k#O>6t3aUM?q52O4XwK+g^BGvnc`A3k3;IPF*iK z(`3{>dgqwkB4WEn#lS|--OIF0Y=`y1=RS@l&Ij*rq~ipx^tGI|%mU?aZ8k2gRSmKNmIzHa1{!VReIqh?7W;)b>0+yG$i} z8+oryNnS0g+FFwB)(NBU^}{0u1nP*p zQUsWJ#`+5(Pc|$}Hrb{E8}Hxg(ju2$;}UTdUKWZOw+}E7M^0SQhnf1#_VdJ{v`5UF zkZ*-%I%18(hq@&#HAIhctOB)L_pn!45P@^8jkJ=!($j~jR%u&R!nNJg%rnVhvD?!w z>Mv#H%j9&2aE2!>#0nPogNFAbRbA=KunH3|j^}2!F)#7TIhrPK?ayXbtpQ{_XrJ{1bwDp!2nltA-)NuduG7!E3k<^N> zh}{b*%OUQ%91Su88Q}!_OptaF2>Obv#rw31^p{{avu*<9{zEIeTnUtPy$2qg<4a-1_Q5p}(ZRE}k$W~AomK>w}m)X@@@F>+5d{0creaodrWSeYP{wvA+w8D4O zy?*vdKB&cF*>_pyfL1*lFHjjaaGYccJ4U_7YO;8zIj# zA5%JuJzVOzv&1zu7}KNfXKXfEoG9)t4#LNbj2kV|9=z(tLF>#>cW|Fi@|6;GE4g6j z5as(((=zL?k3@O&BGmm9%cI93&J~CmaHyQboWvSbqe_myxw7k82RNie^gEoYYstL7c2G^JTdYJ^K0b9~?sQ8woVn3Yz@t3`vrGxhR`aqeBl~$$2H3 zk>r`GzDA|J0y9)j`kE7O(@DK=K2*g1c_f3-}dWI~PlwJ(WQUecrjz&uH%PWemboqYbxw1hYZ%M>*x zXDTd$uWS>X?>xF_`;H^tgf;!8-g&V;bcy@!<>asa6A^KJw{2T*jGiOD_&lb@OH0c~ zFur{QGoSA-LwS)`(UGVrH(svv%)8gOs=VHY#S_WIYlPpPA*OYjl#PF{Wg&ANv34!O zvxsb8TW*QM?Vc^q-(eA-tH%#J*faSUnpe6K(Kv|Ki!{{q zjv!+N-<`*bWg;EREn1 z$4?Vtj`Y!+w7oECX*R%{wMQu6QQab@!dS?dkJ;PTl+x2biAUwx!;2)W5>`@a)8}V$ z)Es&GQF5zDrs2x0s=!WF{=kfEIgPkac?=i9;o6;VT<5<bwx^ic~LJbG}u3M6V2o>%})X^8;&j5kxGoG>8j`^ zd+)cj?7P~YTcUnVRL8%PmU^C$#ANWsa|Y_v404muWfG_T7e~()C2Epv_wOWkT$Wr< zqEFhxjmm}w?Q+?T#~1{;t$Kw#rnPlOO-B~nRXWZXR_G51q&&vAocXo`L4}FwuN+iK zy(Jrr?9%g}4yLX)<+~4$1)J}q-{3RLs%i5)e9eD=xizP-_J_0JDQE+QLVwU?V5dA8 zRwiyJnCIGQ62N^7upA$qSOIzqovZ?#Dsa5xgg`mD>Evv6tZf|WfKIq4O?6Q=KPMfd zCnuAPtaYr6?Mxi$fC<2~pCgVF=aUg4H=tmEcESS&5_}jB1fdQFvj9IoMxNg4q>q=0 z4bb4}WU2B%8!u~1eOo=C>(z}DR%G$sXVB&DYaKJx4bU^wKBpHTu-(^r99&R9AIsVXD{38Ryz{k(~RR#wG zjF&SqF!-3w^6NMl_?XahMh5x)8F27%4brdU;1J-H{i_TDh4KPt-(SW-;4mH_x%)-- z{pwd46pZ8neBj^5L1D)R_;nl%iu_Fmv;sT3K0qq~|L4qH__2o1$`Am?^Q#PaH-KGq zRtC7uZ!*NOX^%fYYy{}w7??RDL;j{`2%HCcc6|^y@;BWB{t6&QzuphfAMEU!0gpzU zwJ#I`{_TBFJpb(dAjgT&nP)&@$9=|rc@JO@|3StBWLRg%A%HyVj0^_;%{QPte^@gQ zjQ6bmpa9A4tUUl3{I_TD{9+>;YaJj*vp)F`JPIa`z`g{sJ$Xw@pqttv%tdEfx?j)_TBRt)EV0Q@HCMgRZ+ literal 0 HcmV?d00001 diff --git a/src/stack-map/frame.sml b/src/stack-map/frame.sml new file mode 100644 index 0000000..a45d05c --- /dev/null +++ b/src/stack-map/frame.sml @@ -0,0 +1,53 @@ +structure Frame = + struct + datatype diff = + Same + | Full + | Chop of int + | Append of int + + fun localsDifference xs ys = + let + fun chop n xs ys = + if n = 3 + then + case (xs, ys) of + ([], []) => Chop n + | _ => Full + else + case (xs, ys) of + ([], []) => Chop n + | (_ :: xs, []) => chop (n + 1) xs [] + | (_ :: xs, VerificationType.Top :: ys) => chop (n + 1) xs ys + | _ => Full + + fun append n xs ys = + if n = 3 + then + case (xs, ys) of + ([], []) => Append n + | _ => Full + else + case (xs, ys) of + ([], []) => Append n + | ([], _ :: ys) => append (n + 1) [] ys + | (VerificationType.Top :: xs, _ :: ys) => append (n + 1) xs ys + | _ => Full + + fun same xs ys = + case (xs, ys) of + ([], []) => Same + | ([], _ :: ys) => append 1 [] ys + | (_ :: xs, []) => chop 1 xs [] + | (x :: xs, y :: ys) => + if x = y + then same xs ys + else + case (x, y) of + (VerificationType.Top, _) => append 1 xs ys + | (_, VerificationType.Top) => chop 1 xs ys + | _ => Full + in + same xs ys + end + end diff --git a/src/stack-map/stack-lang.sml b/src/stack-map/stack-lang.sml new file mode 100644 index 0000000..be8f9c6 --- /dev/null +++ b/src/stack-map/stack-lang.sml @@ -0,0 +1,267 @@ +structure StackLang = + struct + type local_index = int + + datatype t = + Push of VerificationType.t + | Pop of VerificationType.t + | Load of local_index * VerificationType.t + | Store of local_index * VerificationType.t + | Local of local_index * VerificationType.t + | Branch of { targetOffset : int } + + exception StackUnderflow + + fun interpret instrs = + let + fun generateFrame instrs state = + let + (* TODO: handle longs and doubles which occupy two slots *) + fun fold (instr, { stack, locals, frameMap }) = + case instr of + Push vType => { + stack = vType :: stack, + locals = locals, + frameMap = frameMap + } + | Pop vType => { + stack = List.tl stack handle Empty => raise StackUnderflow, + locals = locals, + frameMap = frameMap + } + | Load (index, vType) => { + stack = vType :: stack, + locals = locals, + frameMap = frameMap + } + | Local (index, vType) => { + stack = stack, + locals = List.update (locals, index, vType), + frameMap = frameMap + } + | Store (index, vType) => { + stack = List.tl stack handle Empty => raise StackUnderflow, + locals = List.update (locals, index, vType), + frameMap = frameMap + } + | Branch { targetOffset } => + let + val frame = { stack = stack, locals = locals } + val frames = + case IntBinaryMap.find (frameMap, targetOffset) of + NONE => { offset = NONE, frames = [frame] } + | SOME { offset, frames } => { offset = offset, frames = frame :: frames } + in + { + stack = stack, + locals = locals, + frameMap = IntBinaryMap.insert (frameMap, targetOffset, frames) + } + end + + in + List.foldl fold state instrs + end + + fun eval instrss = + let + fun fold (index, { offset, instrs }, { stack, locals, frameMap }) = + let + val frame = { stack = stack, locals = locals } + val frames = + case IntBinaryMap.find (frameMap, index) of + NONE => { offset = SOME offset, frames = [frame] } + | SOME { offset = NONE, frames } => { offset = SOME offset, frames = frame :: frames } + | SOME { offset, frames } => { offset = offset, frames = frame :: frames } + val frameMap = IntBinaryMap.insert (frameMap, index, frames) + in + generateFrame instrs { + stack = stack, + locals = locals, + frameMap = frameMap + } + end + + val seed = { + stack = [], + locals = [VerificationType.Reference, VerificationType.Top, VerificationType.Top], (* TODO *) + frameMap = IntBinaryMap.empty + } + in + List.foldli fold seed instrss + end + + fun unwrapOffset item = + case item of + { offset = NONE, frames } => raise Fail "bug: NONE offset" + | { offset = SOME offset, frames } => { offset = offset, frames = frames } + in + List.map unwrapOffset (IntBinaryMap.listItems (#frameMap (eval instrs))) + end + + fun compile frameSets = + let + fun compile ({ offset, frames }, { prevLocals, compiled, lastOffset }) = + let + val isBranchTarget = List.length frames > 1 + val offsetDelta = offset - lastOffset + in + (* TODO: intersect frames *) + case List.hd frames of + { stack = [], locals } => + let + val localsSize = List.length locals + val lastLocalsSize = List.length prevLocals + val localsDiff = lastLocalsSize - localsSize + val stackMapFrame = + if localsDiff = 0 + then StackMap.Same { offsetDelta = offsetDelta } + else + if localsDiff < 0 + then StackMap.Chop { + offsetDelta = offsetDelta, + minusLocals = localsDiff + } + else StackMap.Append { + offsetDelta = offsetDelta, + extraLocals = localsDiff, + locals = List.drop (locals, lastLocalsSize) + } + in + { + prevLocals = locals, + compiled = (isBranchTarget, stackMapFrame) :: compiled, + lastOffset = offset + } + end + | { stack = [a], locals } => + let + val localsSize = List.length locals + val lastLocalsSize = List.length prevLocals + val localsDiff = lastLocalsSize - localsSize + val stackMapFrame = + if localsDiff = 0 + then StackMap.SameLocals1StackItem { offsetDelta = offsetDelta, stack = a } + else StackMap.Full { + offsetDelta = offsetDelta, + stack = [a], + locals = locals + } + in + { + prevLocals = locals, + compiled = (isBranchTarget, stackMapFrame) :: compiled, + lastOffset = offset + } + end + | { stack, locals } => + let + val stackMapFrame = StackMap.Full { + offsetDelta = offsetDelta, + stack = stack, + locals = locals + } + in + { + prevLocals = locals, + compiled = (isBranchTarget, stackMapFrame) :: compiled, + lastOffset = offset + } + end + end + + val state = { + prevLocals = [], + compiled = [], + lastOffset = 0 + } + in + List.rev (#compiled (List.foldl compile state frameSets)) + end + + fun compileCompact frameSets = + case frameSets of + [] => [] + | { frames = [{ locals, stack }], offset } :: frameSets => + let + fun compile ({ offset, frames }, state as { prevLocals, compiled, prevOffset }) = + let + val isBranchTarget = List.length frames > 1 + val offsetDelta = offset - (if prevOffset = 0 then prevOffset else prevOffset + 1) + in + if not isBranchTarget + then state + else + (* TODO: intersect frames *) + case List.hd frames of + { stack = [], locals } => + let + val stackMapFrame = + case Frame.localsDifference prevLocals locals of + Frame.Same => StackMap.Same { offsetDelta = offsetDelta } + | Frame.Full => StackMap.Full { + offsetDelta = offsetDelta, + stack = [], + locals = locals + } + | Frame.Chop n => StackMap.Chop { + offsetDelta = offsetDelta, + minusLocals = n + } + | Frame.Append n => StackMap.Append { + offsetDelta = offsetDelta, + extraLocals = n, + locals = List.drop (locals, List.length locals - n) + } + in + { + prevLocals = locals, + compiled = stackMapFrame :: compiled, + prevOffset = offset + } + end + | { stack = [a], locals } => + let + val localsSize = List.length locals + val lastLocalsSize = List.length prevLocals + val localsDiff = lastLocalsSize - localsSize + val stackMapFrame = + if localsDiff = 0 + then StackMap.SameLocals1StackItem { offsetDelta = offsetDelta, stack = a } + else StackMap.Full { + offsetDelta = offsetDelta, + stack = [a], + locals = locals + } + in + { + prevLocals = locals, + compiled = stackMapFrame :: compiled, + prevOffset = offset + } + end + | { stack, locals } => + let + val stackMapFrame = StackMap.Full { + offsetDelta = offsetDelta, + stack = stack, + locals = locals + } + in + { + prevLocals = locals, + compiled = stackMapFrame :: compiled, + prevOffset = offset + } + end + end + + val state = { + prevOffset = 0, + prevLocals = locals, + compiled = [] + } + in + List.rev (#compiled (List.foldl compile state frameSets)) + end + end diff --git a/src/stack-map/stack-map.sml b/src/stack-map/stack-map.sml new file mode 100644 index 0000000..7b62f76 --- /dev/null +++ b/src/stack-map/stack-map.sml @@ -0,0 +1,112 @@ +(* §4.7.4 *) +structure StackMap = + struct + datatype frame = + (* + * This frame type indicates that the frame has exactly the same local + * variables as the previous frame and that the operand stack is empty. + *) + Same of { offsetDelta : int } + + (* + * This frame type indicates that the frame has exactly the same local + * variables as the previous frame and that the operand stack has one + * entry. + *) + | SameLocals1StackItem of { + offsetDelta : int, + stack: VerificationType.t + } + + (* + * This frame type indicates that the frame has the same local variables + * as the previous frame except that the last k local variables are + * absent, and that the operand stack is empty. + *) + | Chop of { + offsetDelta : int, + minusLocals : int + } + + (* + * This frame type indicates that the frame has the same locals as the + * previous frame except that k additional locals are defined, and that + * the operand stack is empty. + *) + | Append of { + offsetDelta : int, + extraLocals : int, + locals : VerificationType.t list + } + + (* + * This frame contains all the stack and locals information, explicitly. + *) + | Full of { + offsetDelta : int, + locals : VerificationType.t list, + stack : VerificationType.t list + } + + open Util + + fun compile constPool frame = + case frame of + Same { offsetDelta } => + if offsetDelta <= 63 + then (u1 offsetDelta, constPool) + else (Word8Vector.prepend (0w251, u2 offsetDelta), constPool) + | SameLocals1StackItem { offsetDelta, stack } => + let + val (vtype, constPool) = VerificationType.compile constPool stack + in + if offsetDelta <= 63 + then (Word8Vector.concat [u1 (offsetDelta + 64), vtype], constPool) + else (Word8Vector.concat [u1 247, u2 offsetDelta, vtype], constPool) + end + | Chop { minusLocals, offsetDelta } => + if minusLocals < 1 orelse minusLocals > 3 + then raise Fail ("chop frame with invalid minusLocals value: " ^ Int.toString minusLocals) + else (Word8Vector.concat [u1 (251 - minusLocals), u2 offsetDelta], constPool) + | Append { extraLocals, offsetDelta, locals } => + if extraLocals < 1 orelse extraLocals > 3 + then raise Fail ("append frame with invalid extraLocals value: " ^ Int.toString extraLocals) + else + let + val (localBytes, constPool) = VerificationType.compileList constPool locals + val bytes = Word8Vector.concat [ + u1 (251 + extraLocals), + u2 offsetDelta, + localBytes + ] + in + (bytes, constPool) + end + | Full { offsetDelta, locals, stack } => + let + val (localBytes, constPool) = VerificationType.compileList constPool locals + val (stackBytes, constPool) = VerificationType.compileList constPool stack + val bytes = Word8Vector.concat [ + u1 255, + u2 offsetDelta, + u2 (List.length locals), + localBytes, + u2 (List.length stack), + stackBytes + ] + in + (bytes, constPool) + end + + fun compileFrames constPool frames = + let + fun fold (frame, (bytes, constPool)) = + let + val (frameBytes, constPool) = compile constPool frame + in + (Word8Vector.concat [bytes, frameBytes], constPool) + end + in + List.foldl fold (vec [], constPool) frames + end + end diff --git a/src/stack-map/verification-type.sml b/src/stack-map/verification-type.sml new file mode 100644 index 0000000..29fda16 --- /dev/null +++ b/src/stack-map/verification-type.sml @@ -0,0 +1,87 @@ +structure VerificationType = + struct + open Util + + datatype t = + Top + | Integer + | Float + | Long + | Double + | Null + | Array of t + | Object of ClassName.t + | Uninitialized of Instr.offset + | UninitializedThis + | Reference + + fun isTop Top = true + | isTop _ = false + + fun fromSimple simple = + case simple of + Descriptor.Bool => Integer + | Descriptor.Byte => Integer + | Descriptor.Char => Integer + | Descriptor.Double => Double + | Descriptor.Float => Float + | Descriptor.Int => Integer + | Descriptor.Long => Long + | Descriptor.Short => Integer + | Descriptor.Object class => Object class + | Descriptor.Array elem => Array (fromSimple elem) + + fun methodReturn descriptor = + case descriptor of + Descriptor.Method { return = Descriptor.Void, ... } => Top + | Descriptor.Method { return = Descriptor.Type simple, ... } => fromSimple simple + | _ => raise Fail "illegal: descriptor is not a method" + + fun methodParams descriptor = + case descriptor of + Descriptor.Method { params, ... } => List.map fromSimple params + | _ => raise Fail "illegal: descriptor is not a method" + + fun fromDescriptor descriptor = + case descriptor of + Descriptor.Raw text => raise Fail "not implemented" + | Descriptor.Method { params, return } => raise Fail "not implemented" + | Descriptor.Field simple => fromSimple simple + + fun fromConst const = + case const of + Const.Integer _ => Integer + | Const.Float _ => Float + | Const.Long _ => Long + | Const.Double _ => Double + | Const.String _ => Object (ClassName.fromParts ["java", "lang", "String"]) + | Const.Class _ => Object (ClassName.fromParts ["java", "lang", "Class"]) + | Const.MethodType _ => Object (ClassName.fromParts ["java", "lang", "invoke", "MethodType"]) + | Const.MethodHandle _ => Object (ClassName.fromParts ["java", "lang", "invoke", "MethodHandle"]) + + fun compile constPool vtype = + case vtype of + Top => (u1 0, constPool) + | Integer => (u1 1, constPool) + | Float => (u1 2, constPool) + | Long => (u1 4, constPool) + | Double => (u1 3, constPool) + | Null => (u1 5, constPool) + | Array t => raise Fail "not implemented" + | Object t => raise Fail "not implemented" + | Uninitialized offset => raise Fail "not implemented" + | UninitializedThis => (u1 6, constPool) + | Reference => raise Fail "not implemented" + + fun compileList constPool vtypes = + let + fun fold (vtype, (bytes, constPool)) = + let + val (newBytes, constPool) = compile constPool vtype + in + (Word8Vector.concat [bytes, newBytes], constPool) + end + in + List.foldl fold (vec [], constPool) vtypes + end + end diff --git a/src/stack-map/verifier.sig b/src/stack-map/verifier.sig new file mode 100644 index 0000000..86fb2e1 --- /dev/null +++ b/src/stack-map/verifier.sig @@ -0,0 +1,4 @@ +signature VERIFIER = + sig + val verify : Instr.t list -> StackLang.t list list + end diff --git a/src/stack-map/verifier.sml b/src/stack-map/verifier.sml new file mode 100644 index 0000000..86766e7 --- /dev/null +++ b/src/stack-map/verifier.sml @@ -0,0 +1,251 @@ +structure Verifier = + struct + open Instr StackLang + + fun verify instrs = + let + fun transition instr = + case instr of + nop => [] + | aconst_null => raise Fail "not implemented: aconst_null" + | iconst_m1 => [Push VerificationType.Integer] + | iconst_0 => [Push VerificationType.Integer] + | iconst_1 => [Push VerificationType.Integer] + | iconst_2 => [Push VerificationType.Integer] + | iconst_3 => [Push VerificationType.Integer] + | iconst_4 => [Push VerificationType.Integer] + | iconst_5 => [Push VerificationType.Integer] + | lconst_0 => raise Fail "not implemented: lconst_0" + | lconst_1 => raise Fail "not implemented: lconst_1" + | fconst_0 => raise Fail "not implemented: fconst_0" + | fconst_1 => raise Fail "not implemented: fconst_1" + | fconst_2 => raise Fail "not implemented: fconst_2" + | dconst_0 => raise Fail "not implemented: dconst_0" + | dconst_1 => raise Fail "not implemented: dconst_1" + | bipush word => raise Fail "not implemented: bipush" + | sipush short => raise Fail "not implemented: sipush" + | ldc const => [Push (VerificationType.fromConst const)] + | iload index => raise Fail "not implemented: iload" + | lload index => raise Fail "not implemented: lload" + | fload index => raise Fail "not implemented: fload" + | dload index => raise Fail "not implemented: dload" + | aload index => raise Fail "not implemented: aload" + | iload_0 => [Load (0, VerificationType.Integer)] + | iload_1 => [Load (1, VerificationType.Integer)] + | iload_2 => [Load (2, VerificationType.Integer)] + | iload_3 => [Load (3, VerificationType.Integer)] + | lload_0 => raise Fail "not implemented: lload_0" + | lload_1 => raise Fail "not implemented: lload_1" + | lload_2 => raise Fail "not implemented: lload_2" + | lload_3 => raise Fail "not implemented: lload_3" + | fload_0 => raise Fail "not implemented: fload_0" + | fload_1 => raise Fail "not implemented: fload_1" + | fload_2 => raise Fail "not implemented: fload_2" + | fload_3 => raise Fail "not implemented: fload_3" + | dload_0 => raise Fail "not implemented: dload_0" + | dload_1 => raise Fail "not implemented: dload_1" + | dload_2 => raise Fail "not implemented: dload_2" + | dload_3 => raise Fail "not implemented: dload_3" + | aload_0 => [Load (0, VerificationType.Reference)] + | aload_1 => [Load (1, VerificationType.Reference)] + | aload_2 => [Load (2, VerificationType.Reference)] + | aload_3 => [Load (3, VerificationType.Reference)] + | iaload => raise Fail "not implemented: iaload" + | laload => raise Fail "not implemented: laload" + | faload => raise Fail "not implemented: faload" + | daload => raise Fail "not implemented: daload" + | aaload => raise Fail "not implemented: aaload" + | baload => raise Fail "not implemented: baload" + | caload => raise Fail "not implemented: caload" + | saload => raise Fail "not implemented: saload" + | istore index => raise Fail "not implemented: istore" + | lstore index => raise Fail "not implemented: lstore" + | fstore index => raise Fail "not implemented: fstore" + | dstore index => raise Fail "not implemented: dstore" + | astore index => raise Fail "not implemented: astore" + | istore_0 => [Store (0, VerificationType.Integer)] + | istore_1 => [Store (1, VerificationType.Integer)] + | istore_2 => [Store (2, VerificationType.Integer)] + | istore_3 => [Store (3, VerificationType.Integer)] + | lstore_0 => raise Fail "not implemented: lstore_0" + | lstore_1 => raise Fail "not implemented: lstore_1" + | lstore_2 => raise Fail "not implemented: lstore_2" + | lstore_3 => raise Fail "not implemented: lstore_3" + | fstore_0 => raise Fail "not implemented: fstore_0" + | fstore_1 => raise Fail "not implemented: fstore_1" + | fstore_2 => raise Fail "not implemented: fstore_2" + | fstore_3 => raise Fail "not implemented: fstore_3" + | dstore_0 => raise Fail "not implemented: dstore_0" + | dstore_1 => raise Fail "not implemented: dstore_1" + | dstore_2 => raise Fail "not implemented: dstore_2" + | dstore_3 => raise Fail "not implemented: dstore_3" + | astore_0 => raise Fail "not implemented: astore_0" + | astore_1 => raise Fail "not implemented: astore_1" + | astore_2 => raise Fail "not implemented: astore_2" + | astore_3 => raise Fail "not implemented: astore_3" + | iastore => raise Fail "not implemented: iastore" + | lastore => raise Fail "not implemented: lastore" + | fastore => raise Fail "not implemented: fastore" + | dastore => raise Fail "not implemented: dastore" + | aastore => raise Fail "not implemented: aastore" + | bastore => raise Fail "not implemented: bastore" + | castore => raise Fail "not implemented: castore" + | sastore => raise Fail "not implemented: sastore" + | pop => raise Fail "not implemented: pop" + | pop2 => raise Fail "not implemented: pop2" + | dup => raise Fail "not implemented: dup" + | dup_x1 => raise Fail "not implemented: dup_x1" + | dup_x2 => raise Fail "not implemented: dup_x2" + | dup2 => raise Fail "not implemented: dup2" + | dup2_x1 => raise Fail "not implemented: dup2_x1" + | dup2_x2 => raise Fail "not implemented: dup2_x2" + | swap => raise Fail "not implemented: swap" + | iadd => raise Fail "not implemented: iadd" + | ladd => raise Fail "not implemented: ladd" + | fadd => raise Fail "not implemented: fadd" + | dadd => raise Fail "not implemented: dadd" + | isub => raise Fail "not implemented: isub" + | lsub => raise Fail "not implemented: lsub" + | fsub => raise Fail "not implemented: fsub" + | dsub => raise Fail "not implemented: dsub" + | imul => [ + Pop VerificationType.Integer, + Pop VerificationType.Integer, + Push VerificationType.Integer + ] + | lmul => raise Fail "not implemented: lmul" + | fmul => raise Fail "not implemented: fmul" + | dmul => raise Fail "not implemented: dmul" + | idiv => raise Fail "not implemented: idiv" + | ldiv => raise Fail "not implemented: ldiv" + | fdiv => raise Fail "not implemented: fdiv" + | ddiv => raise Fail "not implemented: ddiv" + | irem => raise Fail "not implemented: irem" + | lrem => raise Fail "not implemented: lrem" + | frem => raise Fail "not implemented: frem" + | drem => raise Fail "not implemented: drem" + | ineg => raise Fail "not implemented: ineg" + | lneg => raise Fail "not implemented: lneg" + | fneg => raise Fail "not implemented: fneg" + | dneg => raise Fail "not implemented: dneg" + | ishl => raise Fail "not implemented: ishl" + | lshl => raise Fail "not implemented: lshl" + | ishr => raise Fail "not implemented: ishr" + | lshr => raise Fail "not implemented: lshr" + | iushr => raise Fail "not implemented: iushr" + | lushr => raise Fail "not implemented: lushr" + | iand => raise Fail "not implemented: iand" + | land => raise Fail "not implemented: land" + | ior => raise Fail "not implemented: ior" + | lor => raise Fail "not implemented: lor" + | ixor => raise Fail "not implemented: ixor" + | lxor => raise Fail "not implemented: lxor" + | iinc (index, _) => [Local (Word8.toInt index, VerificationType.Integer)] + | i2l => raise Fail "not implemented: i2l" + | i2f => raise Fail "not implemented: i2f" + | i2d => raise Fail "not implemented: i2d" + | l2i => raise Fail "not implemented: l2i" + | l2f => raise Fail "not implemented: l2f" + | l2d => raise Fail "not implemented: l2d" + | f2i => raise Fail "not implemented: f2i" + | f2l => raise Fail "not implemented: f2l" + | f2d => raise Fail "not implemented: f2d" + | d2i => raise Fail "not implemented: d2i" + | d2l => raise Fail "not implemented: d2l" + | d2f => raise Fail "not implemented: d2f" + | i2b => raise Fail "not implemented: i2b" + | i2c => raise Fail "not implemented: i2c" + | i2s => raise Fail "not implemented: i2s" + | lcmp => raise Fail "not implemented: lcmp" + | fcmpl => raise Fail "not implemented: fcmpl" + | fcmpg => raise Fail "not implemented: fcmpg" + | dcmpl => raise Fail "not implemented: dcmpl" + | dcmpg => raise Fail "not implemented: dcmpg" + | ifeq offset => raise Fail "not implemented: ifeq" + | ifne offset => raise Fail "not implemented: ifne" + | iflt offset => raise Fail "not implemented: iflt" + | ifge offset => raise Fail "not implemented: ifge" + | ifgt offset => raise Fail "not implemented: ifgt" + | ifle offset => [ + Pop VerificationType.Integer, + Branch { targetOffset = offset } + ] + | if_icmpeq offset => raise Fail "not implemented: if_icmpeq" + | if_icmpne offset => [ + Pop VerificationType.Integer, + Pop VerificationType.Integer, + Branch { targetOffset = offset } + ] + | if_icmplt offset => raise Fail "not implemented: if_icmplt" + | if_icmpge offset => raise Fail "not implemented: if_icmpge" + | if_icmpgt offset => raise Fail "not implemented: if_icmpgt" + | if_icmple offset => raise Fail "not implemented: if_icmple" + | if_acmpeq offset => raise Fail "not implemented: if_acmpeq" + | if_acmpne offset => raise Fail "not implemented: if_acmpne" + | getstatic { descriptor, ... } => [Push (VerificationType.fromDescriptor descriptor)] + | putstatic _ => raise Fail "not implemented: putstatic" + | getfield _ => raise Fail "not implemented: getfield" + | putfield _ => raise Fail "not implemented: putfield" + | invokevirtual { descriptor, class, ... } => + let + val paramTypes = List.revMap Pop (VerificationType.methodParams descriptor) + val thisType = [Pop (VerificationType.Object class)] + val returnType = + case VerificationType.methodReturn descriptor of + VerificationType.Top => [] + | verificationType => [Push verificationType] + in + List.concat [paramTypes, thisType, returnType] + end + | invokespecial _ => raise Fail "not implemented: invokespecial" + | invokestatic { descriptor, class, ... } => + let + val paramTypes = List.revMap Pop (VerificationType.methodParams descriptor) + val returnType = + case VerificationType.methodReturn descriptor of + VerificationType.Top => [] + | verificationType => [Push verificationType] + in + List.concat [paramTypes, returnType] + end + | invokeinterface _ => raise Fail "not implemented: invokeinterface" + | invokedynamic _ => raise Fail "not implemented: invokedynamic" + | new className => raise Fail "not implemented: new" + | newarray _ => raise Fail "not implemented: newarray" + | anewarray index => raise Fail "not implemented: anewarray" + | arraylength => [ + Pop (VerificationType.Array VerificationType.Top), + Push VerificationType.Integer + ] + | athrow => raise Fail "not implemented: athrow" + | checkcast index => raise Fail "not implemented: checkcast" + | instanceof index => raise Fail "not implemented: instanceof" + | monitorenter => raise Fail "not implemented: monitorenter" + | monitorexit => raise Fail "not implemented: monitorexit" + | goto offset => [Branch { targetOffset = offset }] + | jsr offset => raise Fail "not implemented: jsr" + | ret index => raise Fail "not implemented: ret" + | tableswitch => raise Fail "not implemented: tableswitch" + | lookupswitch => raise Fail "not implemented: lookupswitch" + | ireturn => raise Fail "not implemented: ireturn" + | lreturn => raise Fail "not implemented: lreturn" + | freturn => raise Fail "not implemented: freturn" + | dreturn => raise Fail "not implemented: dreturn" + | areturn => raise Fail "not implemented: areturn" + | return => [Push VerificationType.Top] + | wide => raise Fail "not implemented: wide" + | multianewarray _ => raise Fail "not implemented: multianewarray" + | ifnull offset => raise Fail "not implemented: ifnull" + | ifnonnull offset => raise Fail "not implemented: ifnonnull" + | goto_w offset => raise Fail "not implemented: goto_w" + | jsr_w offset => raise Fail "not implemented: jsr_w" + | breakpoint => raise Fail "not implemented: breakpoint" + | impdep1 => raise Fail "not implemented: impdep1" + | impdep2 => raise Fail "not implemented: impdep2" + in + List.map + (fn (offset, instr) => + { offset = offset, instrs = transition instr }) + instrs + end + end From 15352325a776c6c62fe7c62d89e315315f771dcc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Thu, 4 May 2017 18:37:28 +0300 Subject: [PATCH 05/41] Extend List structure with foldMapState --- lib.cm | 6 ++++++ src/extensions/fn.sig | 9 +++++++++ src/extensions/fn.sml | 6 ++++++ src/extensions/list.sig | 13 +++++++++++++ src/extensions/list.sml | 16 ++++++++++++++++ src/extensions/word8-vector.sml | 6 ++++++ src/stack-map/stack-map.sml | 15 +++++---------- src/stack-map/verification-type.sml | 15 +++++---------- 8 files changed, 66 insertions(+), 20 deletions(-) create mode 100644 src/extensions/fn.sig create mode 100644 src/extensions/fn.sml create mode 100644 src/extensions/list.sig create mode 100644 src/extensions/list.sml create mode 100644 src/extensions/word8-vector.sml diff --git a/lib.cm b/lib.cm index 8ead60a..fba32e7 100644 --- a/lib.cm +++ b/lib.cm @@ -25,6 +25,12 @@ is src/util.sig src/util.sml + src/extensions/fn.sig + src/extensions/fn.sml + src/extensions/list.sig + src/extensions/list.sml + src/extensions/word8-vector.sml + src/stack-map/frame.sml src/stack-map/stack-lang.sml src/stack-map/stack-map.sml diff --git a/src/extensions/fn.sig b/src/extensions/fn.sig new file mode 100644 index 0000000..9b2aae1 --- /dev/null +++ b/src/extensions/fn.sig @@ -0,0 +1,9 @@ +signature FN = + sig + include FN + + (** + * Like `flip`, but for curried functions. + *) + val swap : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c + end diff --git a/src/extensions/fn.sml b/src/extensions/fn.sml new file mode 100644 index 0000000..f137ab6 --- /dev/null +++ b/src/extensions/fn.sml @@ -0,0 +1,6 @@ +structure Fn : FN = + struct + open Fn + + fun swap f a b = f b a + end diff --git a/src/extensions/list.sig b/src/extensions/list.sig new file mode 100644 index 0000000..0472428 --- /dev/null +++ b/src/extensions/list.sig @@ -0,0 +1,13 @@ +signature LIST = + sig + include LIST + + val foldMapState : + 'a list + -> { + monoid : 'b -> 'b -> 'b, + step : 'a -> 's -> ('b * 's), + seed : 'b * 's + } + -> ('b * 's) + end diff --git a/src/extensions/list.sml b/src/extensions/list.sml new file mode 100644 index 0000000..49e2f23 --- /dev/null +++ b/src/extensions/list.sml @@ -0,0 +1,16 @@ +structure List : LIST = + struct + open List + + fun foldMapState list { monoid, step, seed } = + let + fun fold (elem, (r1, state)) = + let + val (r2, state) = step elem state + in + (monoid r1 r2, state) + end + in + List.foldl fold seed list + end + end diff --git a/src/extensions/word8-vector.sml b/src/extensions/word8-vector.sml new file mode 100644 index 0000000..8daadd2 --- /dev/null +++ b/src/extensions/word8-vector.sml @@ -0,0 +1,6 @@ +structure Word8Vector = + struct + open Word8Vector + + fun join a b = concat [a, b] + end diff --git a/src/stack-map/stack-map.sml b/src/stack-map/stack-map.sml index 7b62f76..307de59 100644 --- a/src/stack-map/stack-map.sml +++ b/src/stack-map/stack-map.sml @@ -99,14 +99,9 @@ structure StackMap = end fun compileFrames constPool frames = - let - fun fold (frame, (bytes, constPool)) = - let - val (frameBytes, constPool) = compile constPool frame - in - (Word8Vector.concat [bytes, frameBytes], constPool) - end - in - List.foldl fold (vec [], constPool) frames - end + List.foldMapState frames { + monoid = Word8Vector.join, + step = Fn.swap compile, + seed = (vec [], constPool) + } end diff --git a/src/stack-map/verification-type.sml b/src/stack-map/verification-type.sml index 29fda16..35bd14e 100644 --- a/src/stack-map/verification-type.sml +++ b/src/stack-map/verification-type.sml @@ -74,14 +74,9 @@ structure VerificationType = | Reference => raise Fail "not implemented" fun compileList constPool vtypes = - let - fun fold (vtype, (bytes, constPool)) = - let - val (newBytes, constPool) = compile constPool vtype - in - (Word8Vector.concat [bytes, newBytes], constPool) - end - in - List.foldl fold (vec [], constPool) vtypes - end + List.foldMapState vtypes { + monoid = Word8Vector.join, + step = Fn.swap compile, + seed = (vec [], constPool) + } end From 6a7324675fdd4b9398354313f4a66e2e31ea378e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Thu, 4 May 2017 18:43:15 +0300 Subject: [PATCH 06/41] Remove unused as-pattern --- src/labeled-instr.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index bd2685d..b562311 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -235,7 +235,7 @@ structure LabeledInstr = fun compileList constPool instrs = let fun traverse [] state = state - | traverse (instr :: rest) (state as { index, offset, constPool, stackSize, maxStack, maxLocals, bytes, seenLabels, offsetedInstrs }) = + | traverse (instr :: rest) { index, offset, constPool, stackSize, maxStack, maxLocals, bytes, seenLabels, offsetedInstrs } = case instr of GOTO { label, instr, byteCount } => let in case LabelMap.find (seenLabels, label) of From 99cf07f11d7ff73e31d9b7872f72953fd4715e08 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Thu, 4 May 2017 18:44:10 +0300 Subject: [PATCH 07/41] Reorder members in structure --- src/labeled-instr.sml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index b562311..8d18aac 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -221,17 +221,17 @@ structure LabeledInstr = val impdep1 = INSTR Instr.impdep1 val impdep2 = INSTR Instr.impdep2 - structure LabelMap = BinaryMapFn(struct - type ord_key = string - val compare = String.compare - end) - fun toString instr = case instr of INSTR instr => "INSTR " ^ Instr.toString instr | LABEL label => "LABEL " ^ label | GOTO { label, instr, ... } => "GOTO (" ^ label ^ ", " ^ Instr.toString (instr 0) ^ ")" + structure LabelMap = BinaryMapFn(struct + type ord_key = string + val compare = String.compare + end) + fun compileList constPool instrs = let fun traverse [] state = state From 767f6f7465505ba3ed9efe030374e5c3693f8165 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Thu, 4 May 2017 23:59:39 +0300 Subject: [PATCH 08/41] Compute a method's maximum locals --- src/instr.sml | 29 +++++++++++++++++++++++++++++ src/labeled-instr.sml | 5 +++-- 2 files changed, 32 insertions(+), 2 deletions(-) diff --git a/src/instr.sml b/src/instr.sml index 1443ac2..1fa052e 100644 --- a/src/instr.sml +++ b/src/instr.sml @@ -277,6 +277,35 @@ structure Instr = infix +: val op +: = Word8Vector.prepend infix :+ val op :+ = Word8Vector.append + fun storeIndex instr = + case instr of + istore i => SOME (Word8.toInt i) + | lstore i => SOME (Word8.toInt i) + | fstore i => SOME (Word8.toInt i) + | dstore i => SOME (Word8.toInt i) + | astore i => SOME (Word8.toInt i) + | istore_0 => SOME 0 + | lstore_0 => SOME 0 + | fstore_0 => SOME 0 + | dstore_0 => SOME 0 + | astore_0 => SOME 0 + | istore_1 => SOME 1 + | lstore_1 => SOME 1 + | fstore_1 => SOME 1 + | dstore_1 => SOME 1 + | astore_1 => SOME 1 + | istore_2 => SOME 2 + | lstore_2 => SOME 2 + | fstore_2 => SOME 2 + | dstore_2 => SOME 2 + | astore_2 => SOME 2 + | istore_3 => SOME 3 + | lstore_3 => SOME 3 + | fstore_3 => SOME 3 + | dstore_3 => SOME 3 + | astore_3 => SOME 3 + | _ => NONE + fun compile constPool instr = case instr of nop => (vec [0wx0], 0, constPool) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index 8d18aac..8dac5ab 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -329,6 +329,7 @@ structure LabeledInstr = | INSTR instr => let val (opcodes, stackDiff, constPool) = Instr.compile constPool instr + val storeIndex = Option.getOpt (Instr.storeIndex instr, 0) + 1 in traverse rest { index = index + 1, @@ -336,7 +337,7 @@ structure LabeledInstr = constPool = constPool, stackSize = stackSize + stackDiff, maxStack = Int.max (maxStack, stackSize + stackDiff), - maxLocals = maxLocals, + maxLocals = Int.max (maxLocals, storeIndex), bytes = Word8Vector.concat [bytes, opcodes], seenLabels = seenLabels, offsetedInstrs = (offset, instr) :: offsetedInstrs @@ -349,7 +350,7 @@ structure LabeledInstr = constPool = constPool, stackSize = 0, maxStack = 0, - maxLocals = 10, (* TODO: compute maxLocals *) + maxLocals = 0, bytes = Util.vec [], seenLabels = LabelMap.empty, offsetedInstrs = [] From a7281ca5047fbf0e313074532ffbaebb9b2e25f4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Fri, 5 May 2017 01:14:32 +0300 Subject: [PATCH 09/41] Fix bug in the max stack calculation When we encounter a GOTO instruction for which we haven't encountered the label yet, then we don't know its stackDiff contribution until after the continuation traversal has finished. That's why we reset the stackSize and maxStack counters and compensate for this later on when we know the stackDiff contribution of the branching instruction. --- src/labeled-instr.sml | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index 8dac5ab..d6a8e52 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -268,8 +268,12 @@ structure LabeledInstr = index = index + 1, offset = offset + byteCount, constPool = constPool, - stackSize = stackSize, - maxStack = maxStack, + (* + * We don't have an instruction stackDiff here, so + * we just reset these counter and compensate later. + *) + stackSize = 0, + maxStack = 0, maxLocals = maxLocals, bytes = Util.vec [], seenLabels = seenLabels, @@ -297,7 +301,12 @@ structure LabeledInstr = offset = #offset result, (* TODO: check this is correct *) constPool = constPool, stackSize = stackSize + stackDiff, - maxStack = Int.max (#maxStack result, stackSize + stackDiff), + (* + * Here's where we compensate for the fact that + * above we didn't know the stack diff amount of + * an instruction. + *) + maxStack = Int.max (maxStack, #maxStack result + stackSize + stackDiff), maxLocals = #maxLocals result, seenLabels = #seenLabels result, bytes = Word8Vector.concat [ From c8a338357f5f94045cf6b83c6bae03b5d1e7806d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Fri, 5 May 2017 01:28:34 +0300 Subject: [PATCH 10/41] Complete TODO marker --- src/labeled-instr.sml | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index d6a8e52..5b8302c 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -297,10 +297,22 @@ structure LabeledInstr = Instr.compile (#constPool result) instr in { - index = index + 1, - offset = #offset result, (* TODO: check this is correct *) + (* + * These values are only read inside recursive + * calls, not when the function returns, so nobody + * will look at them, which means we can use default + * values and save some computations. + *) + index = 0, + offset = 0, + stackSize = 0, + seenLabels = LabelMap.empty, + + (* + * The following are values that will be read on + * return, so we have to put the real values. + *) constPool = constPool, - stackSize = stackSize + stackDiff, (* * Here's where we compensate for the fact that * above we didn't know the stack diff amount of @@ -308,7 +320,6 @@ structure LabeledInstr = *) maxStack = Int.max (maxStack, #maxStack result + stackSize + stackDiff), maxLocals = #maxLocals result, - seenLabels = #seenLabels result, bytes = Word8Vector.concat [ bytes, opcodes, From 91e30cab1d0f03cf9481993bc144dc89589c9365 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Fri, 5 May 2017 01:29:45 +0300 Subject: [PATCH 11/41] Use pattern matching instead of record accessors Makes it obvious what values are actually needed. --- src/labeled-instr.sml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index 5b8302c..6588a64 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -376,14 +376,15 @@ structure LabeledInstr = offsetedInstrs = [] } - val result = traverse instrs seed + val { bytes, maxStack, maxLocals, constPool, offsetedInstrs, ... } = + traverse instrs seed in { - bytes = #bytes result, - maxStack = #maxStack result, - maxLocals = #maxLocals result, - constPool = #constPool result, - offsetedInstrs = List.rev (#offsetedInstrs result) + bytes = bytes, + maxStack = maxStack, + maxLocals = maxLocals, + constPool = constPool, + offsetedInstrs = List.rev offsetedInstrs } end end From d89a10ef3101915ffcd2243ff492b810d1bbd3a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Fri, 5 May 2017 01:31:18 +0300 Subject: [PATCH 12/41] Reorder match cases from simple to complex --- src/labeled-instr.sml | 60 +++++++++++++++++++++---------------------- 1 file changed, 30 insertions(+), 30 deletions(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index 6588a64..d61f35f 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -237,7 +237,36 @@ structure LabeledInstr = fun traverse [] state = state | traverse (instr :: rest) { index, offset, constPool, stackSize, maxStack, maxLocals, bytes, seenLabels, offsetedInstrs } = case instr of - GOTO { label, instr, byteCount } => let in + LABEL label => + traverse rest { + index = index, + offset = offset, + constPool = constPool, + stackSize = stackSize, + maxStack = maxStack, + maxLocals = maxLocals, + bytes = bytes, + seenLabels = LabelMap.insert (seenLabels, label, (offset, index)), + offsetedInstrs = offsetedInstrs + } + | INSTR instr => + let + val (opcodes, stackDiff, constPool) = Instr.compile constPool instr + val storeIndex = Option.getOpt (Instr.storeIndex instr, 0) + 1 + in + traverse rest { + index = index + 1, + offset = offset + Word8Vector.length opcodes, + constPool = constPool, + stackSize = stackSize + stackDiff, + maxStack = Int.max (maxStack, stackSize + stackDiff), + maxLocals = Int.max (maxLocals, storeIndex), + bytes = Word8Vector.concat [bytes, opcodes], + seenLabels = seenLabels, + offsetedInstrs = (offset, instr) :: offsetedInstrs + } + end + | GOTO { label, instr, byteCount } => let in case LabelMap.find (seenLabels, label) of SOME (labelOffset, labelIndex) => let @@ -334,35 +363,6 @@ structure LabeledInstr = end end end - | LABEL label => - traverse rest { - index = index, - offset = offset, - constPool = constPool, - stackSize = stackSize, - maxStack = maxStack, - maxLocals = maxLocals, - bytes = bytes, - seenLabels = LabelMap.insert (seenLabels, label, (offset, index)), - offsetedInstrs = offsetedInstrs - } - | INSTR instr => - let - val (opcodes, stackDiff, constPool) = Instr.compile constPool instr - val storeIndex = Option.getOpt (Instr.storeIndex instr, 0) + 1 - in - traverse rest { - index = index + 1, - offset = offset + Word8Vector.length opcodes, - constPool = constPool, - stackSize = stackSize + stackDiff, - maxStack = Int.max (maxStack, stackSize + stackDiff), - maxLocals = Int.max (maxLocals, storeIndex), - bytes = Word8Vector.concat [bytes, opcodes], - seenLabels = seenLabels, - offsetedInstrs = (offset, instr) :: offsetedInstrs - } - end val seed = { index = 0, From b91f177558265237a4d1fce003ed950b9958af88 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Fri, 5 May 2017 01:33:07 +0300 Subject: [PATCH 13/41] Typo --- src/labeled-instr.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index d61f35f..03fc1c9 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -299,7 +299,7 @@ structure LabeledInstr = constPool = constPool, (* * We don't have an instruction stackDiff here, so - * we just reset these counter and compensate later. + * we just reset these counters and compensate later. *) stackSize = 0, maxStack = 0, From 24e2467392856138def8dcac2a918f848f2fd0c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Fri, 5 May 2017 01:38:49 +0300 Subject: [PATCH 14/41] Formatting --- src/labeled-instr.sml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index 03fc1c9..97c7ef0 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -347,7 +347,10 @@ structure LabeledInstr = * above we didn't know the stack diff amount of * an instruction. *) - maxStack = Int.max (maxStack, #maxStack result + stackSize + stackDiff), + maxStack = Int.max ( + maxStack, + #maxStack result + stackSize + stackDiff + ), maxLocals = #maxLocals result, bytes = Word8Vector.concat [ bytes, From df0d984e2fe7459906724c8cd7a21e83f89a6e61 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Fri, 5 May 2017 01:38:58 +0300 Subject: [PATCH 15/41] Reduce line lengths using this weird trick --- src/labeled-instr.sml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index 97c7ef0..73ced91 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -235,7 +235,11 @@ structure LabeledInstr = fun compileList constPool instrs = let fun traverse [] state = state - | traverse (instr :: rest) { index, offset, constPool, stackSize, maxStack, maxLocals, bytes, seenLabels, offsetedInstrs } = + | traverse (instr :: rest) state = + let + val { index, offset, constPool, stackSize, maxStack, ... } = state + val { maxLocals, bytes, seenLabels, offsetedInstrs, ... } = state + in case instr of LABEL label => traverse rest { @@ -366,6 +370,7 @@ structure LabeledInstr = end end end + end val seed = { index = 0, From 5f18606d120b215dcc23b76a6d7731f1ad74cc1a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Fri, 5 May 2017 01:55:06 +0300 Subject: [PATCH 16/41] Convert match cases into helper functions --- src/labeled-instr.sml | 281 ++++++++++++++++++++++-------------------- 1 file changed, 146 insertions(+), 135 deletions(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index 73ced91..f6f1c24 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -225,7 +225,8 @@ structure LabeledInstr = case instr of INSTR instr => "INSTR " ^ Instr.toString instr | LABEL label => "LABEL " ^ label - | GOTO { label, instr, ... } => "GOTO (" ^ label ^ ", " ^ Instr.toString (instr 0) ^ ")" + | GOTO { label, instr, ... } => + "GOTO (" ^ label ^ ", " ^ Instr.toString (instr 0) ^ ")" structure LabelMap = BinaryMapFn(struct type ord_key = string @@ -234,143 +235,153 @@ structure LabeledInstr = fun compileList constPool instrs = let - fun traverse [] state = state - | traverse (instr :: rest) state = - let - val { index, offset, constPool, stackSize, maxStack, ... } = state - val { maxLocals, bytes, seenLabels, offsetedInstrs, ... } = state - in - case instr of - LABEL label => - traverse rest { - index = index, - offset = offset, - constPool = constPool, - stackSize = stackSize, - maxStack = maxStack, - maxLocals = maxLocals, - bytes = bytes, - seenLabels = LabelMap.insert (seenLabels, label, (offset, index)), - offsetedInstrs = offsetedInstrs - } - | INSTR instr => - let - val (opcodes, stackDiff, constPool) = Instr.compile constPool instr - val storeIndex = Option.getOpt (Instr.storeIndex instr, 0) + 1 - in - traverse rest { - index = index + 1, - offset = offset + Word8Vector.length opcodes, - constPool = constPool, - stackSize = stackSize + stackDiff, - maxStack = Int.max (maxStack, stackSize + stackDiff), - maxLocals = Int.max (maxLocals, storeIndex), - bytes = Word8Vector.concat [bytes, opcodes], - seenLabels = seenLabels, - offsetedInstrs = (offset, instr) :: offsetedInstrs - } - end - | GOTO { label, instr, byteCount } => let in - case LabelMap.find (seenLabels, label) of - SOME (labelOffset, labelIndex) => - let - val offsetedInstr = instr labelIndex - val instr = instr (labelOffset - offset) - val (opcodes, stackDiff, constPool) = Instr.compile constPool instr - in - traverse rest { - index = index + 1, - offset = offset + Word8Vector.length opcodes, - constPool = constPool, - stackSize = stackSize + stackDiff, - maxStack = Int.max (maxStack, stackSize + stackDiff), - maxLocals = maxLocals, - bytes = Word8Vector.concat [bytes, opcodes], - seenLabels = seenLabels, - offsetedInstrs = (offset, offsetedInstr) :: offsetedInstrs - } - end - | NONE => - let + fun traverseLabel label state rest = + let + val { index, offset, constPool, stackSize, maxStack, ... } = state + val { maxLocals, bytes, seenLabels, offsetedInstrs, ... } = state + in + traverse rest { + index = index, + offset = offset, + constPool = constPool, + stackSize = stackSize, + maxStack = maxStack, + maxLocals = maxLocals, + bytes = bytes, + seenLabels = LabelMap.insert (seenLabels, label, (offset, index)), + offsetedInstrs = offsetedInstrs + } + end + + and traverseInstr instr state rest = + let + val { index, offset, constPool, stackSize, maxStack, ... } = state + val { maxLocals, bytes, seenLabels, offsetedInstrs, ... } = state + val (opcodes, stackDiff, constPool) = Instr.compile constPool instr + val storeIndex = Option.getOpt (Instr.storeIndex instr, 0) + 1 + in + traverse rest { + index = index + 1, + offset = offset + Word8Vector.length opcodes, + constPool = constPool, + stackSize = stackSize + stackDiff, + maxStack = Int.max (maxStack, stackSize + stackDiff), + maxLocals = Int.max (maxLocals, storeIndex), + bytes = Word8Vector.concat [bytes, opcodes], + seenLabels = seenLabels, + offsetedInstrs = (offset, instr) :: offsetedInstrs + } + end + + and traverseGoto { label, instr, byteCount } state rest = + let + val { index, offset, constPool, stackSize, maxStack, ... } = state + val { maxLocals, bytes, seenLabels, offsetedInstrs, ... } = state + in + case LabelMap.find (seenLabels, label) of + SOME (labelOffset, labelIndex) => + let + val offsetedInstr = instr labelIndex + val instr = instr (labelOffset - offset) + val (opcodes, stackDiff, constPool) = Instr.compile constPool instr + in + traverse rest { + index = index + 1, + offset = offset + Word8Vector.length opcodes, + constPool = constPool, + stackSize = stackSize + stackDiff, + maxStack = Int.max (maxStack, stackSize + stackDiff), + maxLocals = maxLocals, + bytes = Word8Vector.concat [bytes, opcodes], + seenLabels = seenLabels, + offsetedInstrs = (offset, offsetedInstr) :: offsetedInstrs + } + end + | NONE => + let + (* + * We don't have a label yet; traverse the rest of the + * instruction stream and then try again, maybe a label + * has been found. + *) + val result = traverse rest { + index = index + 1, + offset = offset + byteCount, + constPool = constPool, + (* + * We don't have an instruction stackDiff here, so we just + * reset these counters and compensate later. + *) + stackSize = 0, + maxStack = 0, + maxLocals = maxLocals, + bytes = Util.vec [], + seenLabels = seenLabels, + offsetedInstrs = [] + } + in + case LabelMap.find (#seenLabels result, label) of + NONE => raise Fail ("undefined label: " ^ label) + | SOME (labelOffset, labelIndex) => + let + (* + * We're doing a kind of a dirty thing here. We're misusing + * the instruction's offset field by putting the *index* of + * the target instruction. The index as it appears in our + * instruction list, not in the final byte stream. + *) + val offsetedInstr = instr labelIndex + val instr = instr (labelOffset - offset) + val (opcodes, stackDiff, constPool) = + Instr.compile (#constPool result) instr + in + { + (* + * These values are only read inside recursive calls, not + * when the function returns, so nobody will look at them, + * which means we can use default values and save some + * computations. + *) + index = 0, + offset = 0, + stackSize = 0, + seenLabels = LabelMap.empty, + + (* + * The following are values that will be read on return, + * so we have to put the real values. + *) + constPool = constPool, (* - * We don't have a label yet; traverse the rest of the - * instruction stream and then try again, maybe a label - * has been found. + * Here's where we compensate for the fact that above we + * didn't know the stack diff amount of an instruction. *) - val result = traverse rest { - index = index + 1, - offset = offset + byteCount, - constPool = constPool, - (* - * We don't have an instruction stackDiff here, so - * we just reset these counters and compensate later. - *) - stackSize = 0, - maxStack = 0, - maxLocals = maxLocals, - bytes = Util.vec [], - seenLabels = seenLabels, - offsetedInstrs = [] - } - in - case LabelMap.find (#seenLabels result, label) of - NONE => raise Fail ("undefined label: " ^ label) - | SOME (labelOffset, labelIndex) => - let - (* - * We're doing a kind of a dirty thing here. We're - * misusing the instruction's offset field by putting - * the *index* of the target instruction. The index - * as it appears in our instruction list, not in the - * final byte stream. - *) - val offsetedInstr = instr labelIndex - val instr = instr (labelOffset - offset) - val (opcodes, stackDiff, constPool) = - Instr.compile (#constPool result) instr - in - { - (* - * These values are only read inside recursive - * calls, not when the function returns, so nobody - * will look at them, which means we can use default - * values and save some computations. - *) - index = 0, - offset = 0, - stackSize = 0, - seenLabels = LabelMap.empty, + maxStack = Int.max ( + maxStack, + #maxStack result + stackSize + stackDiff + ), + maxLocals = #maxLocals result, + bytes = Word8Vector.concat [ + bytes, + opcodes, + #bytes result + ], + offsetedInstrs = List.concat [ + #offsetedInstrs result, + [(offset, offsetedInstr)], + offsetedInstrs + ] + } + end + end + end - (* - * The following are values that will be read on - * return, so we have to put the real values. - *) - constPool = constPool, - (* - * Here's where we compensate for the fact that - * above we didn't know the stack diff amount of - * an instruction. - *) - maxStack = Int.max ( - maxStack, - #maxStack result + stackSize + stackDiff - ), - maxLocals = #maxLocals result, - bytes = Word8Vector.concat [ - bytes, - opcodes, - #bytes result - ], - offsetedInstrs = List.concat [ - #offsetedInstrs result, - [(offset, offsetedInstr)], - offsetedInstrs - ] - } - end - end - end - end + and traverse instrs state = + case instrs of + [] => state + | (LABEL label :: rest) => traverseLabel label state rest + | (INSTR instr :: rest) => traverseInstr instr state rest + | (GOTO goto :: rest) => traverseGoto goto state rest val seed = { index = 0, From a012ff8f8de4f198f0b61b70dd93ba414ee60ff9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Fri, 5 May 2017 01:56:14 +0300 Subject: [PATCH 17/41] Inline record --- src/labeled-instr.sml | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index f6f1c24..edeb94c 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -383,20 +383,18 @@ structure LabeledInstr = | (INSTR instr :: rest) => traverseInstr instr state rest | (GOTO goto :: rest) => traverseGoto goto state rest - val seed = { - index = 0, - offset = 0, - constPool = constPool, - stackSize = 0, - maxStack = 0, - maxLocals = 0, - bytes = Util.vec [], - seenLabels = LabelMap.empty, - offsetedInstrs = [] - } - val { bytes, maxStack, maxLocals, constPool, offsetedInstrs, ... } = - traverse instrs seed + traverse instrs { + index = 0, + offset = 0, + constPool = constPool, + stackSize = 0, + maxStack = 0, + maxLocals = 0, + bytes = Util.vec [], + seenLabels = LabelMap.empty, + offsetedInstrs = [] + } in { bytes = bytes, From 9bda2fe9c4daa64cbf8afbc6c2d57c1411285b75 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Fri, 5 May 2017 02:08:25 +0300 Subject: [PATCH 18/41] Convert match cases into helper functions --- src/stack-map/stack-map.sml | 67 ++++++++++++++++++++++--------------- 1 file changed, 40 insertions(+), 27 deletions(-) diff --git a/src/stack-map/stack-map.sml b/src/stack-map/stack-map.sml index 307de59..46f30cf 100644 --- a/src/stack-map/stack-map.sml +++ b/src/stack-map/stack-map.sml @@ -51,24 +51,27 @@ structure StackMap = open Util fun compile constPool frame = - case frame of - Same { offsetDelta } => + let + fun same { offsetDelta } = if offsetDelta <= 63 then (u1 offsetDelta, constPool) else (Word8Vector.prepend (0w251, u2 offsetDelta), constPool) - | SameLocals1StackItem { offsetDelta, stack } => - let - val (vtype, constPool) = VerificationType.compile constPool stack - in - if offsetDelta <= 63 - then (Word8Vector.concat [u1 (offsetDelta + 64), vtype], constPool) - else (Word8Vector.concat [u1 247, u2 offsetDelta, vtype], constPool) - end - | Chop { minusLocals, offsetDelta } => + + fun sameLocals1StackItem { offsetDelta, stack } = + let + val (vtype, constPool) = VerificationType.compile constPool stack + in + if offsetDelta <= 63 + then (Word8Vector.concat [u1 (offsetDelta + 64), vtype], constPool) + else (Word8Vector.concat [u1 247, u2 offsetDelta, vtype], constPool) + end + + fun chop { minusLocals, offsetDelta } = if minusLocals < 1 orelse minusLocals > 3 then raise Fail ("chop frame with invalid minusLocals value: " ^ Int.toString minusLocals) else (Word8Vector.concat [u1 (251 - minusLocals), u2 offsetDelta], constPool) - | Append { extraLocals, offsetDelta, locals } => + + fun append { extraLocals, offsetDelta, locals } = if extraLocals < 1 orelse extraLocals > 3 then raise Fail ("append frame with invalid extraLocals value: " ^ Int.toString extraLocals) else @@ -82,21 +85,31 @@ structure StackMap = in (bytes, constPool) end - | Full { offsetDelta, locals, stack } => - let - val (localBytes, constPool) = VerificationType.compileList constPool locals - val (stackBytes, constPool) = VerificationType.compileList constPool stack - val bytes = Word8Vector.concat [ - u1 255, - u2 offsetDelta, - u2 (List.length locals), - localBytes, - u2 (List.length stack), - stackBytes - ] - in - (bytes, constPool) - end + + fun full { offsetDelta, locals, stack } = + let + val (localBytes, constPool) = VerificationType.compileList constPool locals + val (stackBytes, constPool) = VerificationType.compileList constPool stack + val bytes = Word8Vector.concat [ + u1 255, + u2 offsetDelta, + u2 (List.length locals), + localBytes, + u2 (List.length stack), + stackBytes + ] + in + (bytes, constPool) + end + + in + case frame of + Same a => same a + | SameLocals1StackItem a => sameLocals1StackItem a + | Chop a => chop a + | Append a => append a + | Full a => full a + end fun compileFrames constPool frames = List.foldMapState frames { From ebf5957da527228ec11c9e5b9e13d5cf4fb43538 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Fri, 5 May 2017 18:56:56 +0300 Subject: [PATCH 19/41] Fix label handling bug in LabeledInstr It turns out seen labels are actually read on return. --- src/labeled-instr.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index edeb94c..6ace578 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -345,13 +345,13 @@ structure LabeledInstr = index = 0, offset = 0, stackSize = 0, - seenLabels = LabelMap.empty, (* * The following are values that will be read on return, * so we have to put the real values. *) constPool = constPool, + seenLabels = #seenLabels result, (* * Here's where we compensate for the fact that above we * didn't know the stack diff amount of an instruction. From 7409abbacbc2935fa2b2a27a69f96a0d55532d99 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Sat, 6 May 2017 16:10:20 +0300 Subject: [PATCH 20/41] Add VerificationType.toString --- src/stack-map/verification-type.sml | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/stack-map/verification-type.sml b/src/stack-map/verification-type.sml index 35bd14e..848b232 100644 --- a/src/stack-map/verification-type.sml +++ b/src/stack-map/verification-type.sml @@ -15,6 +15,20 @@ structure VerificationType = | UninitializedThis | Reference + fun toString t = + case t of + Top => "Top" + | Integer => "Integer" + | Float => "Float" + | Long => "Long" + | Double => "Double" + | Null => "Null" + | Array _ => "Array" + | Object _ => "Object" + | Uninitialized _ => "Uninitialized" + | UninitializedThis => "UninitializedThis" + | Reference => "Reference" + fun isTop Top = true | isTop _ = false From 9fe91354e9807b482ea5bf1b299ce6c1f6b3fa14 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Sat, 6 May 2017 16:19:56 +0300 Subject: [PATCH 21/41] Merge frames on branch target instructions --- src/main.sml | 54 ++++++++++- src/stack-map/stack-lang.sml | 143 ++++++++++++++++++++-------- src/stack-map/verification-type.sml | 9 ++ src/stack-map/verifier.sml | 22 +++-- 4 files changed, 180 insertions(+), 48 deletions(-) diff --git a/src/main.sml b/src/main.sml index 440a03f..a5af38b 100644 --- a/src/main.sml +++ b/src/main.sml @@ -196,7 +196,7 @@ structure Main = iload_1, imul, istore_2, - iinc (0w1, Word8.fromInt ~1), + iinc (0w1, ~ 0w1), goto "enter-while", label "exit-while", getstatic java.lang.System.out, @@ -209,6 +209,54 @@ structure Main = ] } + val nestedLoops = Method.from { + name = "main", + accessFlags = [Method.Flag.PUBLIC, Method.Flag.STATIC], + descriptor = Descriptor.Method { + return = Descriptor.Void, + params = [ + Descriptor.Array (Descriptor.Object (ClassName.fromString "java/lang/String")) + ] + }, + attributes = [ + Attr.Code { + exceptionTable = [], + attributes = [], + code = let open Instr in [ + iconst_0, + istore_1, + label "goto-2", + iload_1, + bipush 0w10, + if_icmpge "exit", + iconst_0, + istore_2, + label "goto-1", + iload_2, + bipush 0w10, + if_icmpge "iinc", + getstatic java.lang.System.out, + iload_1, + iload_2, + iadd, + invokestatic java.lang.Integer.toString, + invokevirtual java.io.PrintStream.println, + iinc (0w2, 0w1), + goto "goto-1", + label "iinc", + iinc (0w1, 0w1), + iload_2, + iconst_3, + iadd, + pop, + goto "goto-2", + label "exit", + return + ] end + } + ] + } + val class = Class.from { accessFlags = [Class.Flag.PUBLIC], thisClass = ClassName.fromString "Main", @@ -226,7 +274,7 @@ structure Main = } ], (* methods = [main, printString, bootstrap] *) - methods = [factorial] + methods = [nestedLoops] } val trim = @@ -257,7 +305,7 @@ structure Main = fun stackMap () = let - val { attributes = [Attr.Code { code, ... }], ... } = factorial + val { attributes = [Attr.Code { code, ... }], ... } = nestedLoops val { offsetedInstrs, ... } = Instr.compileList ConstPool.empty code in StackLang.compileCompact diff --git a/src/stack-map/stack-lang.sml b/src/stack-map/stack-lang.sml index be8f9c6..ce1318d 100644 --- a/src/stack-map/stack-lang.sml +++ b/src/stack-map/stack-lang.sml @@ -8,97 +8,155 @@ structure StackLang = | Load of local_index * VerificationType.t | Store of local_index * VerificationType.t | Local of local_index * VerificationType.t - | Branch of { targetOffset : int } + | Branch of { targetOffset : int, fallsThrough : bool } exception StackUnderflow + exception UnassignedLocal + + fun toString t = + case t of + Push vtype => "Push " ^ VerificationType.toString vtype + | Pop vtype => "Pop " ^ VerificationType.toString vtype + | Load (index, vtype) => "Load ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" + | Store (index, vtype) => "Store ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" + | Local (index, vtype) => "Local ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" + | Branch { targetOffset, fallsThrough } => + "Branch { targetOffset = "^ Int.toString targetOffset ^", fallsThrough = "^ Bool.toString fallsThrough ^" }" fun interpret instrs = let + fun mergeFrames prev curr = + let + val { stack = prevStack, locals = prevLocals } = prev + val { stack = currStack, locals = currLocals } = curr + in + if List.length prevStack <> List.length currStack + then raise Fail "mergeFrames: different stack lengths" + else + let + val mergedLocals = + ListPair.map (Fn.uncurry VerificationType.leastUpperBound) (prevLocals, currLocals) + in + { + stack = currStack, + locals = mergedLocals + } + end + end + fun generateFrame instrs state = let (* TODO: handle longs and doubles which occupy two slots *) - fun fold (instr, { stack, locals, frameMap }) = + fun fold (instr, { stack, locals, frameMap, fallsThrough }) = case instr of Push vType => { stack = vType :: stack, locals = locals, - frameMap = frameMap + frameMap = frameMap, + fallsThrough = true } | Pop vType => { stack = List.tl stack handle Empty => raise StackUnderflow, locals = locals, - frameMap = frameMap + frameMap = frameMap, + fallsThrough = true } | Load (index, vType) => { stack = vType :: stack, locals = locals, - frameMap = frameMap + frameMap = frameMap, + fallsThrough = true } | Local (index, vType) => { stack = stack, - locals = List.update (locals, index, vType), - frameMap = frameMap + locals = List.update (locals, index, vType) handle Subscript => raise UnassignedLocal, + frameMap = frameMap, + fallsThrough = true } | Store (index, vType) => { stack = List.tl stack handle Empty => raise StackUnderflow, - locals = List.update (locals, index, vType), - frameMap = frameMap + locals = List.update (locals, index, vType) handle Subscript => raise UnassignedLocal, + frameMap = frameMap, + fallsThrough = true } - | Branch { targetOffset } => + | Branch { targetOffset, fallsThrough } => let val frame = { stack = stack, locals = locals } - val frames = + val mergedFrame = case IntBinaryMap.find (frameMap, targetOffset) of - NONE => { offset = NONE, frames = [frame] } - | SOME { offset, frames } => { offset = offset, frames = frame :: frames } + NONE => { offset = NONE, frame = frame, isBranchTarget = true } + | SOME { offset, frame = prevFrame, isBranchTarget } => { + offset = offset, + frame = mergeFrames prevFrame frame, + isBranchTarget = true + } in { stack = stack, locals = locals, - frameMap = IntBinaryMap.insert (frameMap, targetOffset, frames) + frameMap = IntBinaryMap.insert (frameMap, targetOffset, mergedFrame), + fallsThrough = fallsThrough } end - in List.foldl fold state instrs end fun eval instrss = let - fun fold (index, { offset, instrs }, { stack, locals, frameMap }) = + fun fold (index, { offset, instrs }, { stack, locals, frameMap, fallsThrough }) = let val frame = { stack = stack, locals = locals } - val frames = + val mergedFrame = case IntBinaryMap.find (frameMap, index) of - NONE => { offset = SOME offset, frames = [frame] } - | SOME { offset = NONE, frames } => { offset = SOME offset, frames = frame :: frames } - | SOME { offset, frames } => { offset = offset, frames = frame :: frames } - val frameMap = IntBinaryMap.insert (frameMap, index, frames) + NONE => { + offset = SOME offset, + frame = frame, + isBranchTarget = false + } + | SOME { offset = NONE, frame = prevFrame, isBranchTarget } => { + offset = SOME offset, + frame = mergeFrames prevFrame frame, + isBranchTarget = isBranchTarget + } + | SOME { offset, frame = prevFrame, isBranchTarget } => { + offset = offset, + frame = mergeFrames prevFrame frame, + isBranchTarget = isBranchTarget + } + val frameMap = IntBinaryMap.insert (frameMap, index, mergedFrame) in generateFrame instrs { - stack = stack, + stack = if fallsThrough then stack else [], locals = locals, - frameMap = frameMap + frameMap = frameMap, + fallsThrough = true } end val seed = { stack = [], locals = [VerificationType.Reference, VerificationType.Top, VerificationType.Top], (* TODO *) - frameMap = IntBinaryMap.empty + frameMap = IntBinaryMap.empty, + fallsThrough = true } in List.foldli fold seed instrss end - fun unwrapOffset item = + fun unwrapOffset (index, item) = case item of - { offset = NONE, frames } => raise Fail "bug: NONE offset" - | { offset = SOME offset, frames } => { offset = offset, frames = frames } + { offset = NONE, ... } => raise Fail ("bug: NONE offset at index: " ^ Int.toString index) + | { offset = SOME offset, frame, isBranchTarget } => { + offset = offset, + frame = frame, + isBranchTarget = isBranchTarget + } in - List.map unwrapOffset (IntBinaryMap.listItems (#frameMap (eval instrs))) + List.mapi unwrapOffset (IntBinaryMap.listItems (#frameMap (eval instrs))) end + (* TODO: update function *) fun compile frameSets = let fun compile ({ offset, frames }, { prevLocals, compiled, lastOffset }) = @@ -106,7 +164,6 @@ structure StackLang = val isBranchTarget = List.length frames > 1 val offsetDelta = offset - lastOffset in - (* TODO: intersect frames *) case List.hd frames of { stack = [], locals } => let @@ -182,18 +239,18 @@ structure StackLang = fun compileCompact frameSets = case frameSets of [] => [] - | { frames = [{ locals, stack }], offset } :: frameSets => + | { frame = { locals, stack }, offset, isBranchTarget } :: frameSets => let - fun compile ({ offset, frames }, state as { prevLocals, compiled, prevOffset }) = + fun compile ({ offset, frame, isBranchTarget }, state as { prevLocals, compiled, prevOffset }) = let - val isBranchTarget = List.length frames > 1 + (* val isBranchTarget = List.length frames > 1 *) val offsetDelta = offset - (if prevOffset = 0 then prevOffset else prevOffset + 1) in if not isBranchTarget then state else (* TODO: intersect frames *) - case List.hd frames of + case frame of { stack = [], locals } => let val stackMapFrame = @@ -208,11 +265,21 @@ structure StackLang = offsetDelta = offsetDelta, minusLocals = n } - | Frame.Append n => StackMap.Append { - offsetDelta = offsetDelta, - extraLocals = n, - locals = List.drop (locals, List.length locals - n) - } + | Frame.Append n => + let + val locals = + case List.drop (locals, List.length locals - n) of + [a, VerificationType.Top, VerificationType.Top] => [a] + | [a, b, VerificationType.Top] => [a, b] + | [a, VerificationType.Top] => [a] + | other => other + in + StackMap.Append { + offsetDelta = offsetDelta, + extraLocals = List.length locals, + locals = locals + } + end in { prevLocals = locals, diff --git a/src/stack-map/verification-type.sml b/src/stack-map/verification-type.sml index 848b232..cd80566 100644 --- a/src/stack-map/verification-type.sml +++ b/src/stack-map/verification-type.sml @@ -29,6 +29,15 @@ structure VerificationType = | UninitializedThis => "UninitializedThis" | Reference => "Reference" + fun leastUpperBound a b = + case (a, b) of + (Top, _) => Top + | (_, Top) => Top + | (a, b) => + if a = b + then a + else raise Fail "not implemented: leastUpperBound" (* TODO *) + fun isTop Top = true | isTop _ = false diff --git a/src/stack-map/verifier.sml b/src/stack-map/verifier.sml index 86766e7..f88cefc 100644 --- a/src/stack-map/verifier.sml +++ b/src/stack-map/verifier.sml @@ -22,7 +22,7 @@ structure Verifier = | fconst_2 => raise Fail "not implemented: fconst_2" | dconst_0 => raise Fail "not implemented: dconst_0" | dconst_1 => raise Fail "not implemented: dconst_1" - | bipush word => raise Fail "not implemented: bipush" + | bipush word => [Push VerificationType.Integer] | sipush short => raise Fail "not implemented: sipush" | ldc const => [Push (VerificationType.fromConst const)] | iload index => raise Fail "not implemented: iload" @@ -91,7 +91,7 @@ structure Verifier = | bastore => raise Fail "not implemented: bastore" | castore => raise Fail "not implemented: castore" | sastore => raise Fail "not implemented: sastore" - | pop => raise Fail "not implemented: pop" + | pop => [Pop VerificationType.Top] | pop2 => raise Fail "not implemented: pop2" | dup => raise Fail "not implemented: dup" | dup_x1 => raise Fail "not implemented: dup_x1" @@ -100,7 +100,11 @@ structure Verifier = | dup2_x1 => raise Fail "not implemented: dup2_x1" | dup2_x2 => raise Fail "not implemented: dup2_x2" | swap => raise Fail "not implemented: swap" - | iadd => raise Fail "not implemented: iadd" + | iadd => [ + Pop VerificationType.Integer, + Pop VerificationType.Integer, + Push VerificationType.Integer + ] | ladd => raise Fail "not implemented: ladd" | fadd => raise Fail "not implemented: fadd" | dadd => raise Fail "not implemented: dadd" @@ -168,16 +172,20 @@ structure Verifier = | ifgt offset => raise Fail "not implemented: ifgt" | ifle offset => [ Pop VerificationType.Integer, - Branch { targetOffset = offset } + Branch { targetOffset = offset, fallsThrough = true } ] | if_icmpeq offset => raise Fail "not implemented: if_icmpeq" | if_icmpne offset => [ Pop VerificationType.Integer, Pop VerificationType.Integer, - Branch { targetOffset = offset } + Branch { targetOffset = offset, fallsThrough = true } ] | if_icmplt offset => raise Fail "not implemented: if_icmplt" - | if_icmpge offset => raise Fail "not implemented: if_icmpge" + | if_icmpge offset => [ + Pop VerificationType.Integer, + Pop VerificationType.Integer, + Branch { targetOffset = offset, fallsThrough = true } + ] | if_icmpgt offset => raise Fail "not implemented: if_icmpgt" | if_icmple offset => raise Fail "not implemented: if_icmple" | if_acmpeq offset => raise Fail "not implemented: if_acmpeq" @@ -222,7 +230,7 @@ structure Verifier = | instanceof index => raise Fail "not implemented: instanceof" | monitorenter => raise Fail "not implemented: monitorenter" | monitorexit => raise Fail "not implemented: monitorexit" - | goto offset => [Branch { targetOffset = offset }] + | goto offset => [Branch { targetOffset = offset, fallsThrough = false }] | jsr offset => raise Fail "not implemented: jsr" | ret index => raise Fail "not implemented: ret" | tableswitch => raise Fail "not implemented: tableswitch" From 358f9e0b26dfb9fa4350a82df81de6897aec1d01 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Sat, 6 May 2017 16:42:11 +0300 Subject: [PATCH 22/41] Add StackMapTable attribute only if not already present Computing it conditionally is still left to be done. --- src/attr.sml | 45 ++++++++++++++++++++++++++++++--------------- src/main.sml | 17 ++++++++++++++++- 2 files changed, 46 insertions(+), 16 deletions(-) diff --git a/src/attr.sml b/src/attr.sml index b7ee006..67e2438 100644 --- a/src/attr.sml +++ b/src/attr.sml @@ -26,7 +26,7 @@ structure Attr = exceptionTable : ExceptionInfo.t list, attributes : t list } - | StackMapTable of (Instr.offset * Instr.t) list + | StackMapTable of StackMap.frame list | Exceptions of ClassName.t list | BootstrapMethods of ConstPool.bootstrap_method list | InnerClasses @@ -48,6 +48,9 @@ structure Attr = | LocalVariableTypeTable | Deprecated + fun isStackMapTable attr = + case attr of StackMapTable _ => true | _ => false + fun compile constPool attr = case attr of Code code => compileCode constPool code @@ -58,7 +61,7 @@ structure Attr = | Signature typeSignature => compileSignature constPool typeSignature | SourceFile value => compileSourceFile constPool value | BootstrapMethods methods => compileBootstrapMethods constPool methods - | StackMapTable instrs => compileStackMapTable constPool instrs + | StackMapTable frames => compileStackMapTable constPool frames | attribute => raise Fail "not implemented" (* https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.3 *) @@ -67,36 +70,46 @@ structure Attr = fun compileExceptions constPool exceptionTable = (u2 0, constPool) (* TODO: add exceptions *) - fun compileAttributes constPool attributes = + fun compileAttributes constPool stackMapTable attributes = let - fun fold (attr, { bytes, length, constPool }) = + fun fold (attr, { bytes, length, constPool, seenStackMapTable }) = let val (attrBytes, constPool) = compile constPool attr in { bytes = Word8Vector.concat [bytes, attrBytes], length = length + 1, - constPool = constPool + constPool = constPool, + seenStackMapTable = seenStackMapTable orelse isStackMapTable attr } end val seed = { bytes = vec [], length = 0, - constPool = constPool + constPool = constPool, + seenStackMapTable = false } - val { bytes, length, constPool } = List.foldl fold seed attributes - val bytes = Word8Vector.concat [u2 length, bytes] + val { bytes, length, constPool, seenStackMapTable } = + List.foldl fold seed attributes in - (bytes, constPool) + if seenStackMapTable + then (Word8Vector.concat [u2 length, bytes], constPool) + else + let + val (attrBytes, constPool) = compile constPool stackMapTable + val bytes = Word8Vector.concat [bytes, attrBytes] + in + (Word8Vector.concat [u2 (length + 1), bytes], constPool) + end end val (attrNameIndex, constPool) = ConstPool.withUtf8 constPool "Code" (* TODO: generate and add StackMapTable only if version >= 50 *) - val (instrBytes, constPool, stackMapTable) = compileInstructions constPool code + val (instrBytes, constPool, stackMapAttr) = compileInstructions constPool code val (exceptionBytes, constPool) = compileExceptions constPool exceptionTable - val (attributeBytes, constPool) = compileAttributes constPool (stackMapTable :: attributes) + val (attributeBytes, constPool) = compileAttributes constPool stackMapAttr attributes val attributeLength = Word8Vector.length instrBytes + Word8Vector.length exceptionBytes + @@ -115,7 +128,10 @@ structure Attr = and compileInstructions constPool code = let val result = LabeledInstr.compileList constPool code - val stackMapTable = StackMapTable (#offsetedInstrs result) + val stackMapFrames = + StackLang.compileCompact + (StackLang.interpret (Verifier.verify (#offsetedInstrs result))) + val stackMapAttr = StackMapTable stackMapFrames val bytes = Word8Vector.concat [ u2 (#maxStack result), u2 (#maxLocals result), @@ -123,7 +139,7 @@ structure Attr = (#bytes result) ] in - (bytes, #constPool result, stackMapTable) + (bytes, #constPool result, stackMapAttr) end and compileConstantValue constPool value = @@ -240,9 +256,8 @@ structure Attr = (bytes, constPool) end - and compileStackMapTable constPool instrs = + and compileStackMapTable constPool frames = let - val frames = StackLang.compileCompact (StackLang.interpret (Verifier.verify instrs)) val (stackMapBytes, constPool) = StackMap.compileFrames constPool frames val (attrIndex, constPool) = ConstPool.withUtf8 constPool "StackMapTable" val attributeLength = 2 + Word8Vector.length stackMapBytes diff --git a/src/main.sml b/src/main.sml index a5af38b..58430b9 100644 --- a/src/main.sml +++ b/src/main.sml @@ -221,7 +221,22 @@ structure Main = attributes = [ Attr.Code { exceptionTable = [], - attributes = [], + attributes = [ + (* Attr.StackMapTable [ + StackMap.Append { + offsetDelta = 2, + extraLocals = 1, + locals = [VerificationType.Integer] + }, + StackMap.Append { + offsetDelta = 7, + extraLocals = 1, + locals = [VerificationType.Integer] + }, + StackMap.Same { offsetDelta = 23 }, + StackMap.Chop { minusLocals = 1, offsetDelta = 9 } + ] *) + ], code = let open Instr in [ iconst_0, istore_1, From cca211fc1bf29875e3f567c66c46b673d1160ea2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Sat, 6 May 2017 17:55:59 +0300 Subject: [PATCH 23/41] Create a small framework for composing fold functions --- src/attr.sml | 38 ++++++++++++++++++++------------------ src/extensions/list.sig | 30 ++++++++++++++++++++++++++++++ src/extensions/list.sml | 27 +++++++++++++++++++++++++++ 3 files changed, 77 insertions(+), 18 deletions(-) diff --git a/src/attr.sml b/src/attr.sml index 67e2438..3ef75ac 100644 --- a/src/attr.sml +++ b/src/attr.sml @@ -72,27 +72,29 @@ structure Attr = fun compileAttributes constPool stackMapTable attributes = let - fun fold (attr, { bytes, length, constPool, seenStackMapTable }) = - let - val (attrBytes, constPool) = compile constPool attr - in - { - bytes = Word8Vector.concat [bytes, attrBytes], - length = length + 1, - constPool = constPool, - seenStackMapTable = seenStackMapTable orelse isStackMapTable attr - } - end + open List.Op.<&> infixr <&> + + val detectStackMapTable = { + seed = false, + step = fn (attr, seen) => seen orelse isStackMapTable attr + } - val seed = { - bytes = vec [], - length = 0, - constPool = constPool, - seenStackMapTable = false + val compileAttr = { + seed = { bytes = vec [], length = 0, constPool = constPool }, + step = fn (attr, { bytes, length, constPool }) => + let + val (attrBytes, constPool) = compile constPool attr + in + { + bytes = Word8Vector.concat [bytes, attrBytes], + length = length + 1, + constPool = constPool + } + end } - val { bytes, length, constPool, seenStackMapTable } = - List.foldl fold seed attributes + val (seenStackMapTable, { bytes, length, constPool }) = + List.stepl (detectStackMapTable <&> compileAttr) attributes in if seenStackMapTable then (Word8Vector.concat [u2 length, bytes], constPool) diff --git a/src/extensions/list.sig b/src/extensions/list.sig index 0472428..11b6ccc 100644 --- a/src/extensions/list.sig +++ b/src/extensions/list.sig @@ -2,6 +2,11 @@ signature LIST = sig include LIST + type ('a, 's) stepper = { + seed : 's, + step : 'a * 's -> 's + } + val foldMapState : 'a list -> { @@ -10,4 +15,29 @@ signature LIST = seed : 'b * 's } -> ('b * 's) + + val stepl : ('a, 's) stepper -> 'a list -> 's + val stepr : ('a, 's) stepper -> 'a list -> 's + + structure Op : + sig + (** + * Operator for composing fold functions. + *) + structure & : + sig + val & : + ('a * 'state_1 -> 'state_1) * ('a * 'state_2 -> 'state_2) + -> 'a * ('state_1 * 'state_2) + -> 'state_1 * 'state_2 + end + + (** + * Operator for composing `stepper`s. + *) + structure <&> : + sig + val <&> : ('a, 'b) stepper * ('a, 'c) stepper -> ('a, 'b * 'c) stepper + end + end end diff --git a/src/extensions/list.sml b/src/extensions/list.sml index 49e2f23..760fecc 100644 --- a/src/extensions/list.sml +++ b/src/extensions/list.sml @@ -2,6 +2,11 @@ structure List : LIST = struct open List + type ('a, 's) stepper = { + seed : 's, + step : 'a * 's -> 's + } + fun foldMapState list { monoid, step, seed } = let fun fold (elem, (r1, state)) = @@ -13,4 +18,26 @@ structure List : LIST = in List.foldl fold seed list end + + fun stepl { step, seed } = List.foldl step seed + fun stepr { step, seed } = List.foldr step seed + + structure Op = + struct + structure & = + struct + fun & (f, g) = + fn (elem, (a, b)) => (f (elem, a), g (elem, b)) + end + + structure <&> = + struct + open & infixr & + + fun <&> (f : ('a, 's) stepper, g : ('a, 't) stepper) = { + step = #step f & #step g, + seed = (#seed f, #seed g) + } + end + end end From f4ab7e8f335831854d121a70c715e367f1b4cc45 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Sat, 6 May 2017 18:10:05 +0300 Subject: [PATCH 24/41] Reorder lines --- src/extensions/list.sml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/extensions/list.sml b/src/extensions/list.sml index 760fecc..d55cb84 100644 --- a/src/extensions/list.sml +++ b/src/extensions/list.sml @@ -35,8 +35,8 @@ structure List : LIST = open & infixr & fun <&> (f : ('a, 's) stepper, g : ('a, 't) stepper) = { - step = #step f & #step g, - seed = (#seed f, #seed g) + seed = (#seed f, #seed g), + step = #step f & #step g } end end From 327bb627da9765903c82c8036158f9fbc77c2593 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 24 Apr 2023 16:47:46 +0300 Subject: [PATCH 25/41] Use optional pattern bars; supported by SuccessorML (sML) --- src/attr.sml | 10 +++++----- src/class.sml | 4 ++-- src/const-pool.sml | 18 +++++++++--------- src/const.sml | 2 +- src/descriptor.sml | 16 ++++++++-------- src/field.sml | 4 ++-- src/instr.sml | 14 +++++++------- src/labeled-instr.sml | 10 +++++----- src/method-handle.sml | 4 ++-- src/method.sml | 4 ++-- src/stack-map/frame.sml | 10 +++++----- src/stack-map/stack-lang.sml | 14 +++++++------- src/stack-map/stack-map.sml | 11 +++++------ src/stack-map/verification-type.sml | 16 ++++++++-------- src/stack-map/verifier.sml | 6 +++--- 15 files changed, 71 insertions(+), 72 deletions(-) diff --git a/src/attr.sml b/src/attr.sml index 3ef75ac..0590d89 100644 --- a/src/attr.sml +++ b/src/attr.sml @@ -6,7 +6,7 @@ structure ExceptionInfo = structure ConstantValue = struct datatype t = - Integer of Integer.t + | Integer of Integer.t | Long of Long.t | Float of Float.t | Double of Double.t @@ -19,7 +19,7 @@ structure Attr = open Util datatype t = - Custom + | Custom | ConstantValue of ConstantValue.t | Code of { code : LabeledInstr.t list, @@ -53,7 +53,7 @@ structure Attr = fun compile constPool attr = case attr of - Code code => compileCode constPool code + | Code code => compileCode constPool code | ConstantValue value => compileConstantValue constPool value | Exceptions exceptions => compileExceptions constPool exceptions | Synthetic => compileSynthetic constPool @@ -149,7 +149,7 @@ structure Attr = val (attrNameIndex, constPool) = ConstPool.withUtf8 constPool "ConstantValue" val (constValueIndex, constPool) = case value of - ConstantValue.Integer value => raise Fail "not implemented" + | ConstantValue.Integer value => raise Fail "not implemented" | ConstantValue.Long value => raise Fail "not implemented" | ConstantValue.Float value => raise Fail "not implemented" | ConstantValue.Double value => raise Fail "not implemented" @@ -275,7 +275,7 @@ structure Attr = fun minimumVersion attr = case attr of - Custom => { major = 45, minor = 3 } + | Custom => { major = 45, minor = 3 } | SourceFile _ => { major = 45, minor = 3 } | InnerClasses => { major = 45, minor = 3 } | ConstantValue _ => { major = 45, minor = 3 } diff --git a/src/class.sml b/src/class.sml index 302356b..06c912c 100644 --- a/src/class.sml +++ b/src/class.sml @@ -3,7 +3,7 @@ structure Class = structure Flag = struct datatype t = - PUBLIC + | PUBLIC | FINAL | SUPER | INTERFACE @@ -14,7 +14,7 @@ structure Class = fun compile flag : Word.word = case flag of - PUBLIC => 0wx0001 + | PUBLIC => 0wx0001 | FINAL => 0wx0010 | SUPER => 0wx0020 | INTERFACE => 0wx0200 diff --git a/src/const-pool.sml b/src/const-pool.sml index 9d1e053..249d3aa 100644 --- a/src/const-pool.sml +++ b/src/const-pool.sml @@ -28,7 +28,7 @@ structure ConstPool :> CONST_POOL = end) datatype entry = - Class of entry_index + | Class of entry_index | String of entry_index | Utf8 of Text.t | Long of Long.t @@ -48,7 +48,7 @@ structure ConstPool :> CONST_POOL = fun ordinal entry = case entry of - Class _ => 0 + | Class _ => 0 | String _ => 1 | Utf8 _ => 2 | Long _ => 3 @@ -65,12 +65,12 @@ structure ConstPool :> CONST_POOL = fun tupleCompare ((a, x), (b, y)) = case Int.compare (a, b) of - EQUAL => Int.compare (x, y) + | EQUAL => Int.compare (x, y) | other => other fun compare operands = case operands of - (Class a, Class b) => Int.compare (a, b) + | (Class a, Class b) => Int.compare (a, b) | (String a, String b) => Int.compare (a, b) | (Utf8 a, Utf8 b) => Text.compare (a, b) | (Long a, Long b) => Long.compare (a, b) @@ -109,7 +109,7 @@ structure ConstPool :> CONST_POOL = fun withEntry (constPool as { counter, entries, bootstrap }) entry = case Map.find (entries, entry) of - SOME entryIndex => (entryIndex, constPool) + | SOME entryIndex => (entryIndex, constPool) | NONE => let val counter = counter + 1 @@ -174,7 +174,7 @@ structure ConstPool :> CONST_POOL = open MethodHandle val makeSymbolRef = case kind of - GetField => withSymbolRef Fieldref + | GetField => withSymbolRef Fieldref | GetStatic => withSymbolRef Fieldref | PutField => withSymbolRef Fieldref | PutStatic => withSymbolRef Fieldref @@ -204,7 +204,7 @@ structure ConstPool :> CONST_POOL = let val (index, constPool) = case methodParam of - Const.Integer a => withInteger constPool a + | Const.Integer a => withInteger constPool a | Const.Float a => withFloat constPool a | Const.String a => withString constPool a | Const.Class a => withClass constPool a @@ -226,7 +226,7 @@ structure ConstPool :> CONST_POOL = val entry = { methodRef = methodHandleIndex, arguments = arguments } in case BootstrapMethodsMap.find (bootEntries, entry) of - SOME entryIndex => (entryIndex, constPool) + | SOME entryIndex => (entryIndex, constPool) | NONE => let val newEntries = BootstrapMethodsMap.insert (bootEntries, entry, bootCounter) @@ -268,7 +268,7 @@ structure ConstPool :> CONST_POOL = let val entryBytes = case entry of - Class entryIndex => Word8Vector.concat [vec [0wx7], u2 entryIndex] + | Class entryIndex => Word8Vector.concat [vec [0wx7], u2 entryIndex] | String entryIndex => Word8Vector.concat [vec [0wx8], u2 entryIndex] | Utf8 value => let diff --git a/src/const.sml b/src/const.sml index 1b4c784..9188fe1 100644 --- a/src/const.sml +++ b/src/const.sml @@ -1,7 +1,7 @@ structure Const = struct datatype t = - Integer of Integer.t + | Integer of Integer.t | Float of Float.t | Long of Long.t | Double of Double.t diff --git a/src/descriptor.sml b/src/descriptor.sml index f39b99c..54c93cb 100644 --- a/src/descriptor.sml +++ b/src/descriptor.sml @@ -4,12 +4,12 @@ structure Descriptor = struct datatype t = - Raw of Text.t + | Raw of Text.t | Field of simple | Method of { params : simple list, return : return } and simple = - Bool + | Bool | Byte | Char | Double @@ -21,14 +21,14 @@ structure Descriptor = | Array of simple and return = - Void + | Void | Type of simple fun fromString s = Raw s fun paramsCount descriptor = case descriptor of - Raw d => 1 (* TODO *) + | Raw d => 1 (* TODO *) | Field _ => raise Fail "paramsCount called on field descriptor" | Method { params, ... } => let @@ -43,7 +43,7 @@ structure Descriptor = fun returnCount descriptor = case descriptor of - Method { params, return = Void } => 0 + | Method { params, return = Void } => 0 | Method _ => 1 | Field _ => raise Fail "returnCount called on field descriptor" | Raw d => 0 (* TODO *) @@ -52,7 +52,7 @@ structure Descriptor = let fun simple f = case f of - Byte => "B" + | Byte => "B" | Char => "C" | Double => "D" | Float => "F" @@ -64,11 +64,11 @@ structure Descriptor = | Array elemType => "[" ^ simple elemType fun return r = case r of - Void => "V" + | Void => "V" | Type t => simple t in case descriptor of - Raw d => d + | Raw d => d | Field f => simple f | Method { params, return = r } => "(" ^ String.concat (List.map simple params) ^ ")" ^ return r diff --git a/src/field.sml b/src/field.sml index a4fea04..a31de57 100644 --- a/src/field.sml +++ b/src/field.sml @@ -3,7 +3,7 @@ structure Field = structure Flag = struct datatype t = - PUBLIC + | PUBLIC | PRIVATE | PROTECTED | STATIC @@ -15,7 +15,7 @@ structure Field = fun compile flag : Word.word = case flag of - PUBLIC => 0wx0001 + | PUBLIC => 0wx0001 | PRIVATE => 0wx0002 | PROTECTED => 0wx0004 | STATIC => 0wx0008 diff --git a/src/instr.sml b/src/instr.sml index 1fa052e..5943f38 100644 --- a/src/instr.sml +++ b/src/instr.sml @@ -1,7 +1,7 @@ structure ArrayType = struct datatype t = - BOOLEAN + | BOOLEAN | CHAR | FLOAT | DOUBLE @@ -12,7 +12,7 @@ structure ArrayType = fun compile t : Word8.word = case t of - BOOLEAN => 0w4 + | BOOLEAN => 0w4 | CHAR => 0w5 | FLOAT => 0w6 | DOUBLE => 0w7 @@ -30,7 +30,7 @@ structure Instr = type index = Word8.word datatype t = - nop (* Constants *) + | nop (* Constants *) | aconst_null | iconst_m1 | iconst_0 @@ -279,7 +279,7 @@ structure Instr = fun storeIndex instr = case instr of - istore i => SOME (Word8.toInt i) + | istore i => SOME (Word8.toInt i) | lstore i => SOME (Word8.toInt i) | fstore i => SOME (Word8.toInt i) | dstore i => SOME (Word8.toInt i) @@ -308,7 +308,7 @@ structure Instr = fun compile constPool instr = case instr of - nop => (vec [0wx0], 0, constPool) + | nop => (vec [0wx0], 0, constPool) | aconst_null => (vec [0wx1], 1, constPool) | iconst_m1 => (vec [0wx2], 1, constPool) | iconst_0 => (vec [0wx3], 1, constPool) @@ -345,7 +345,7 @@ structure Instr = end in case const of - Const.Integer a => ldc ConstPool.withInteger a + | Const.Integer a => ldc ConstPool.withInteger a | Const.Float a => ldc ConstPool.withFloat a | Const.String a => ldc ConstPool.withString a | Const.Class a => ldc ConstPool.withClass a @@ -673,7 +673,7 @@ structure Instr = fun toString instr = case instr of - nop => "nop" + | nop => "nop" | aconst_null => "aconst_null" | iconst_m1 => "iconst_m1" | iconst_0 => "iconst_0" diff --git a/src/labeled-instr.sml b/src/labeled-instr.sml index 6ace578..82eefa8 100644 --- a/src/labeled-instr.sml +++ b/src/labeled-instr.sml @@ -8,7 +8,7 @@ structure LabeledInstr = type label = string datatype t = - INSTR of Instr.t + | INSTR of Instr.t | LABEL of label | GOTO of { label : label, @@ -223,7 +223,7 @@ structure LabeledInstr = fun toString instr = case instr of - INSTR instr => "INSTR " ^ Instr.toString instr + | INSTR instr => "INSTR " ^ Instr.toString instr | LABEL label => "LABEL " ^ label | GOTO { label, instr, ... } => "GOTO (" ^ label ^ ", " ^ Instr.toString (instr 0) ^ ")" @@ -279,7 +279,7 @@ structure LabeledInstr = val { maxLocals, bytes, seenLabels, offsetedInstrs, ... } = state in case LabelMap.find (seenLabels, label) of - SOME (labelOffset, labelIndex) => + | SOME (labelOffset, labelIndex) => let val offsetedInstr = instr labelIndex val instr = instr (labelOffset - offset) @@ -321,7 +321,7 @@ structure LabeledInstr = } in case LabelMap.find (#seenLabels result, label) of - NONE => raise Fail ("undefined label: " ^ label) + | NONE => raise Fail ("undefined label: " ^ label) | SOME (labelOffset, labelIndex) => let (* @@ -378,7 +378,7 @@ structure LabeledInstr = and traverse instrs state = case instrs of - [] => state + | [] => state | (LABEL label :: rest) => traverseLabel label state rest | (INSTR instr :: rest) => traverseInstr instr state rest | (GOTO goto :: rest) => traverseGoto goto state rest diff --git a/src/method-handle.sml b/src/method-handle.sml index 4541f4e..08465d5 100644 --- a/src/method-handle.sml +++ b/src/method-handle.sml @@ -1,7 +1,7 @@ structure MethodHandle = struct datatype t = - GetField + | GetField | GetStatic | PutField | PutStatic @@ -13,7 +13,7 @@ structure MethodHandle = fun value kind = case kind of - GetField => 1 + | GetField => 1 | GetStatic => 2 | PutField => 3 | PutStatic => 4 diff --git a/src/method.sml b/src/method.sml index 5247755..0a5232d 100644 --- a/src/method.sml +++ b/src/method.sml @@ -3,7 +3,7 @@ structure Method = structure Flag = struct datatype t = - PUBLIC + | PUBLIC | PRIVATE | PROTECTED | STATIC @@ -18,7 +18,7 @@ structure Method = fun compile flag : Word.word = case flag of - PUBLIC => 0wx0001 + | PUBLIC => 0wx0001 | PRIVATE => 0wx0002 | PROTECTED => 0wx0004 | STATIC => 0wx0008 diff --git a/src/stack-map/frame.sml b/src/stack-map/frame.sml index a45d05c..3d2c920 100644 --- a/src/stack-map/frame.sml +++ b/src/stack-map/frame.sml @@ -1,7 +1,7 @@ structure Frame = struct datatype diff = - Same + | Same | Full | Chop of int | Append of int @@ -25,18 +25,18 @@ structure Frame = if n = 3 then case (xs, ys) of - ([], []) => Append n + | ([], []) => Append n | _ => Full else case (xs, ys) of - ([], []) => Append n + | ([], []) => Append n | ([], _ :: ys) => append (n + 1) [] ys | (VerificationType.Top :: xs, _ :: ys) => append (n + 1) xs ys | _ => Full fun same xs ys = case (xs, ys) of - ([], []) => Same + | ([], []) => Same | ([], _ :: ys) => append 1 [] ys | (_ :: xs, []) => chop 1 xs [] | (x :: xs, y :: ys) => @@ -44,7 +44,7 @@ structure Frame = then same xs ys else case (x, y) of - (VerificationType.Top, _) => append 1 xs ys + | (VerificationType.Top, _) => append 1 xs ys | (_, VerificationType.Top) => chop 1 xs ys | _ => Full in diff --git a/src/stack-map/stack-lang.sml b/src/stack-map/stack-lang.sml index ce1318d..f29f3df 100644 --- a/src/stack-map/stack-lang.sml +++ b/src/stack-map/stack-lang.sml @@ -3,7 +3,7 @@ structure StackLang = type local_index = int datatype t = - Push of VerificationType.t + | Push of VerificationType.t | Pop of VerificationType.t | Load of local_index * VerificationType.t | Store of local_index * VerificationType.t @@ -15,7 +15,7 @@ structure StackLang = fun toString t = case t of - Push vtype => "Push " ^ VerificationType.toString vtype + | Push vtype => "Push " ^ VerificationType.toString vtype | Pop vtype => "Pop " ^ VerificationType.toString vtype | Load (index, vtype) => "Load ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" | Store (index, vtype) => "Store ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" @@ -49,7 +49,7 @@ structure StackLang = (* TODO: handle longs and doubles which occupy two slots *) fun fold (instr, { stack, locals, frameMap, fallsThrough }) = case instr of - Push vType => { + | Push vType => { stack = vType :: stack, locals = locals, frameMap = frameMap, @@ -109,7 +109,7 @@ structure StackLang = val frame = { stack = stack, locals = locals } val mergedFrame = case IntBinaryMap.find (frameMap, index) of - NONE => { + | NONE => { offset = SOME offset, frame = frame, isBranchTarget = false @@ -146,7 +146,7 @@ structure StackLang = fun unwrapOffset (index, item) = case item of - { offset = NONE, ... } => raise Fail ("bug: NONE offset at index: " ^ Int.toString index) + | { offset = NONE, ... } => raise Fail ("bug: NONE offset at index: " ^ Int.toString index) | { offset = SOME offset, frame, isBranchTarget } => { offset = offset, frame = frame, @@ -165,7 +165,7 @@ structure StackLang = val offsetDelta = offset - lastOffset in case List.hd frames of - { stack = [], locals } => + | { stack = [], locals } => let val localsSize = List.length locals val lastLocalsSize = List.length prevLocals @@ -238,7 +238,7 @@ structure StackLang = fun compileCompact frameSets = case frameSets of - [] => [] + | [] => [] | { frame = { locals, stack }, offset, isBranchTarget } :: frameSets => let fun compile ({ offset, frame, isBranchTarget }, state as { prevLocals, compiled, prevOffset }) = diff --git a/src/stack-map/stack-map.sml b/src/stack-map/stack-map.sml index 46f30cf..dd94621 100644 --- a/src/stack-map/stack-map.sml +++ b/src/stack-map/stack-map.sml @@ -6,7 +6,7 @@ structure StackMap = * This frame type indicates that the frame has exactly the same local * variables as the previous frame and that the operand stack is empty. *) - Same of { offsetDelta : int } + | Same of { offsetDelta : int } (* * This frame type indicates that the frame has exactly the same local @@ -101,14 +101,13 @@ structure StackMap = in (bytes, constPool) end - in case frame of - Same a => same a + | Same a => same a | SameLocals1StackItem a => sameLocals1StackItem a - | Chop a => chop a - | Append a => append a - | Full a => full a + | Chop a => chop a + | Append a => append a + | Full a => full a end fun compileFrames constPool frames = diff --git a/src/stack-map/verification-type.sml b/src/stack-map/verification-type.sml index cd80566..a80cd1e 100644 --- a/src/stack-map/verification-type.sml +++ b/src/stack-map/verification-type.sml @@ -17,7 +17,7 @@ structure VerificationType = fun toString t = case t of - Top => "Top" + | Top => "Top" | Integer => "Integer" | Float => "Float" | Long => "Long" @@ -31,7 +31,7 @@ structure VerificationType = fun leastUpperBound a b = case (a, b) of - (Top, _) => Top + | (Top, _) => Top | (_, Top) => Top | (a, b) => if a = b @@ -43,7 +43,7 @@ structure VerificationType = fun fromSimple simple = case simple of - Descriptor.Bool => Integer + | Descriptor.Bool => Integer | Descriptor.Byte => Integer | Descriptor.Char => Integer | Descriptor.Double => Double @@ -56,24 +56,24 @@ structure VerificationType = fun methodReturn descriptor = case descriptor of - Descriptor.Method { return = Descriptor.Void, ... } => Top + | Descriptor.Method { return = Descriptor.Void, ... } => Top | Descriptor.Method { return = Descriptor.Type simple, ... } => fromSimple simple | _ => raise Fail "illegal: descriptor is not a method" fun methodParams descriptor = case descriptor of - Descriptor.Method { params, ... } => List.map fromSimple params + | Descriptor.Method { params, ... } => List.map fromSimple params | _ => raise Fail "illegal: descriptor is not a method" fun fromDescriptor descriptor = case descriptor of - Descriptor.Raw text => raise Fail "not implemented" + | Descriptor.Raw text => raise Fail "not implemented" | Descriptor.Method { params, return } => raise Fail "not implemented" | Descriptor.Field simple => fromSimple simple fun fromConst const = case const of - Const.Integer _ => Integer + | Const.Integer _ => Integer | Const.Float _ => Float | Const.Long _ => Long | Const.Double _ => Double @@ -84,7 +84,7 @@ structure VerificationType = fun compile constPool vtype = case vtype of - Top => (u1 0, constPool) + | Top => (u1 0, constPool) | Integer => (u1 1, constPool) | Float => (u1 2, constPool) | Long => (u1 4, constPool) diff --git a/src/stack-map/verifier.sml b/src/stack-map/verifier.sml index f88cefc..4d33f17 100644 --- a/src/stack-map/verifier.sml +++ b/src/stack-map/verifier.sml @@ -6,7 +6,7 @@ structure Verifier = let fun transition instr = case instr of - nop => [] + | nop => [] | aconst_null => raise Fail "not implemented: aconst_null" | iconst_m1 => [Push VerificationType.Integer] | iconst_0 => [Push VerificationType.Integer] @@ -200,7 +200,7 @@ structure Verifier = val thisType = [Pop (VerificationType.Object class)] val returnType = case VerificationType.methodReturn descriptor of - VerificationType.Top => [] + | VerificationType.Top => [] | verificationType => [Push verificationType] in List.concat [paramTypes, thisType, returnType] @@ -211,7 +211,7 @@ structure Verifier = val paramTypes = List.revMap Pop (VerificationType.methodParams descriptor) val returnType = case VerificationType.methodReturn descriptor of - VerificationType.Top => [] + | VerificationType.Top => [] | verificationType => [Push verificationType] in List.concat [paramTypes, returnType] From fd55fa4390540e4a78a3f9b5f70a0f7c66a8c86b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 24 Apr 2023 16:56:18 +0300 Subject: [PATCH 26/41] Remove symbolic structure names, which are prohibited by the standard --- lib.cm | 6 +++--- src/attr.sml | 2 +- src/extensions/list.sig | 16 +++++----------- src/extensions/list.sml | 21 ++++++++------------- 4 files changed, 17 insertions(+), 28 deletions(-) diff --git a/lib.cm b/lib.cm index fba32e7..db4b915 100644 --- a/lib.cm +++ b/lib.cm @@ -1,9 +1,11 @@ library (0.1.0) + library ($BUCHAREST-ML/sml-foundation/lib.cm) source (-) is - $/basis.cm $/smlnj-lib.cm + $BUCHAREST-ML/sml-foundation/lib.cm + src/attr.sml src/class.sml src/class-name.sml @@ -25,8 +27,6 @@ is src/util.sig src/util.sml - src/extensions/fn.sig - src/extensions/fn.sml src/extensions/list.sig src/extensions/list.sml src/extensions/word8-vector.sml diff --git a/src/attr.sml b/src/attr.sml index 0590d89..7f53c26 100644 --- a/src/attr.sml +++ b/src/attr.sml @@ -72,7 +72,7 @@ structure Attr = fun compileAttributes constPool stackMapTable attributes = let - open List.Op.<&> infixr <&> + open List.Op infixr <&> val detectStackMapTable = { seed = false, diff --git a/src/extensions/list.sig b/src/extensions/list.sig index 11b6ccc..69462f4 100644 --- a/src/extensions/list.sig +++ b/src/extensions/list.sig @@ -24,20 +24,14 @@ signature LIST = (** * Operator for composing fold functions. *) - structure & : - sig - val & : - ('a * 'state_1 -> 'state_1) * ('a * 'state_2 -> 'state_2) - -> 'a * ('state_1 * 'state_2) - -> 'state_1 * 'state_2 - end + val & : + ('a * 'state_1 -> 'state_1) * ('a * 'state_2 -> 'state_2) + -> 'a * ('state_1 * 'state_2) + -> 'state_1 * 'state_2 (** * Operator for composing `stepper`s. *) - structure <&> : - sig - val <&> : ('a, 'b) stepper * ('a, 'c) stepper -> ('a, 'b * 'c) stepper - end + val <&> : ('a, 'b) stepper * ('a, 'c) stepper -> ('a, 'b * 'c) stepper end end diff --git a/src/extensions/list.sml b/src/extensions/list.sml index d55cb84..0678db8 100644 --- a/src/extensions/list.sml +++ b/src/extensions/list.sml @@ -24,20 +24,15 @@ structure List : LIST = structure Op = struct - structure & = - struct - fun & (f, g) = - fn (elem, (a, b)) => (f (elem, a), g (elem, b)) - end + infixr & - structure <&> = - struct - open & infixr & + (* https://smlnj-gforge.cs.uchicago.edu/tracker/?group_id=33&atid=215&func=detail&aid=129 *) + fun f & g = + fn (elem, (a, b)) => (f (elem, a), g (elem, b)) - fun <&> (f : ('a, 's) stepper, g : ('a, 't) stepper) = { - seed = (#seed f, #seed g), - step = #step f & #step g - } - end + fun <&> (f : ('a, 's) stepper, g : ('a, 't) stepper) = { + seed = (#seed f, #seed g), + step = #step f & #step g + } end end From 77aececa29e588098ab2f8a2c0c4eb3a613a9e52 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 24 Apr 2023 16:59:22 +0300 Subject: [PATCH 27/41] Add scaffolding for tests using the sml-test library --- dev.cm | 12 ++++++++++++ readme.md | 18 ++++++++++++++++++ test/all-suites.sml | 5 +++++ test/frame-suite.sml | 18 ++++++++++++++++++ 4 files changed, 53 insertions(+) create mode 100644 dev.cm create mode 100644 test/all-suites.sml create mode 100644 test/frame-suite.sml diff --git a/dev.cm b/dev.cm new file mode 100644 index 0000000..522376e --- /dev/null +++ b/dev.cm @@ -0,0 +1,12 @@ +library (0.1.0) + library (lib.cm) + source (-) +is + $BUCHAREST-ML/sml-test/lib.cm + + lib.cm + + test ( + all-suites.sml + frame-suite.sml + ) diff --git a/readme.md b/readme.md index 8d68c9d..fb22a19 100644 --- a/readme.md +++ b/readme.md @@ -1,5 +1,7 @@ # JVM bytecode assembler in Standard ML +## Running Main + ``` $ sml Standard ML of New Jersey v110.80 [built: Sun Aug 28 21:15:09 2016] @@ -36,3 +38,19 @@ Hello, World! val it = () : unit - ``` + +## Running Tests + +``` +- CM.make "dev.cm"; AllSuites.run (); +[scanning dev.cm] +[scanning $BUCHAREST-ML/sml-test/lib.cm] +[scanning $BUCHAREST-ML/sml-foundation/lib.cm] +[scanning (dev.cm):lib.cm] +[New bindings added.] +val it = true : bool +[+] 1 < 2 +[-] 1 = 1 — NotEqual +val it = () : unit +- +``` diff --git a/test/all-suites.sml b/test/all-suites.sml new file mode 100644 index 0000000..be956c0 --- /dev/null +++ b/test/all-suites.sml @@ -0,0 +1,5 @@ +structure AllSuites = TestRunner( + val all = List.concat [ + FrameSuite.all + ] +) diff --git a/test/frame-suite.sml b/test/frame-suite.sml new file mode 100644 index 0000000..0d0d37b --- /dev/null +++ b/test/frame-suite.sml @@ -0,0 +1,18 @@ +structure FrameSuite : TEST_SUITE = + struct + infix --> + infix === + + open TestSuite + + val all = [ + "1 < 2" --> (fn _ => + Ints.assert 1 op< 2 + ), + + "1 = 1" --> let in fn _ => + 1 === 2 + (* Ints.assert 1 op= 2 *) + end + ] + end From 54f9b924cc5a1b485c2e909a91cc4aa5be134af5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 24 Apr 2023 18:57:14 +0300 Subject: [PATCH 28/41] Use nested directory access syntax in lib.cm --- lib.cm | 60 ++++++++++++++++++++++++++++++---------------------------- 1 file changed, 31 insertions(+), 29 deletions(-) diff --git a/lib.cm b/lib.cm index db4b915..5ee4fa4 100644 --- a/lib.cm +++ b/lib.cm @@ -6,34 +6,36 @@ is $BUCHAREST-ML/sml-foundation/lib.cm - src/attr.sml - src/class.sml - src/class-name.sml - src/const.sml - src/const-pool.sig - src/const-pool.sml - src/descriptor.sml - src/field.sml - src/instr.sml - src/java.sml - src/labeled-instr.sml - src/main.sml - src/member.fun - src/method.sml - src/method-handle.sml - src/prim.sml - src/text.sig - src/text.sml - src/util.sig - src/util.sml + src ( + attr.sml + class.sml + class-name.sml + const.sml + const-pool.sig + const-pool.sml + descriptor.sml + field.sml + instr.sml + java.sml + labeled-instr.sml + main.sml + member.fun + method.sml + method-handle.sml + prim.sml + text.sig + text.sml + util.sig + util.sml - src/extensions/list.sig - src/extensions/list.sml - src/extensions/word8-vector.sml + extensions/list.sig + extensions/list.sml + extensions/word8-vector.sml - src/stack-map/frame.sml - src/stack-map/stack-lang.sml - src/stack-map/stack-map.sml - src/stack-map/verification-type.sml - src/stack-map/verifier.sig - src/stack-map/verifier.sml + stack-map/frame.sml + stack-map/stack-lang.sml + stack-map/stack-map.sml + stack-map/verification-type.sml + stack-map/verifier.sig + stack-map/verifier.sml + ) From 8ea44fb68270cffab57379a8755b29addb85b888 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 24 Apr 2023 19:06:43 +0300 Subject: [PATCH 29/41] Add the Work Log file --- log.md | 156 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 156 insertions(+) create mode 100644 log.md diff --git a/log.md b/log.md new file mode 100644 index 0000000..1b4b2cf --- /dev/null +++ b/log.md @@ -0,0 +1,156 @@ +# Work Log + +## 2023-04-24 09:56:20 + +> Each stack map frame described in the entries table relies on the previous +> frame for some of its semantics. The first stack map frame of a method is +> implicit, and computed from the method descriptor by the type checker +> (§4.10.1.6). The stack_map_frame structure at entries[0] therefore describes +> the second stack map frame of the method. + +— JVMS20, §4.7.4 + +Okay... so I'll have to generate all the stack frames and just after that drop +the ones that are not required by the specification: + +> It is illegal to have code after an **unconditional branch** without a stack +> map frame being provided for it. + +— JVMS20, §4.10.1.6 + +> • Conditional branch: ifeq, ifne, iflt, ifle, ifgt, ifge, ifnull, ifnonnull, if_icmpeq, if_icmpne, if_icmplt, if_icmple, if_icmpgt if_icmpge, if_acmpeq, if_acmpne. +> • Compound conditional branch: tableswitch, lookupswitch. +> • **Unconditional branch**: goto, goto_w, jsr, jsr_w, ret. + +— JVMS20, §2.11.7 + +Steps: + + 1. Build a control-flow graph of the instructions + 2. Basic blocks + +Could we generate the StackMap frames without building the CFG? And only use +a CFG when we want to keep just the required frames? + +--- + +From: From Stack Maps to Software Certificates [slides], slide 6 + +> [Java bytecode verification] is formalized as a data flow problem. + +--- + +Slide 27: + +> BCV typing with interfaces +> Two kind of reference types : classes and interfaces. +> Interfaces introduces a form of intersection types. that must be represented in the type hierarchy. +> The byte code verifier opts for an alternative solution : +> Treat interfaces as java.lang.Object and defer type checking to run-time. +> Type checking rule : +> isJavaAssignable(class(_,_), class(To, L)) :- loadedClass(To, L, ToClass), classIsInterface(ToClass). + +## Efficient Bytecode Verification and Compilation in a Virtual Machine + +Figure 2.1, page 5 + +``` +todo ← true +while todo = true do + todo ← false + for all i in all instructions of a method do + if i was changed then + todo ← true + check whether stack and local variable types match definition of i + calculate new state after i + for all s in all successor instructions of i do + if current state for s ̸= new state derived from i then + assume state after i as new entry state for s + mark s as changed + end if + end for + end if + end for +end while +``` + +## 2023-04-22 22:06:59 + +Taken from a draft in igstan.ro: + +--- +title: JVM Bytecode Verification +author: Ionuț G. Stan +--- + +I'll briefly describe the process of bytecode verification that the JVM +performs during the loading of .class files. + +## Motivation + +Why was verification needed? + +## Complications + +There's a hierarchy of verification types that induces a notion of subtyping. +Store and load instructions need to check subtyping conformance and this +requires loading external classes into the system. I'm hoping to avoid this +somehow, as it requires the side-effect of reading files form disk. In +addition, it means that I might need to write a parser for .class files and a +JAR (which are ZIP archives) reader. + +## 2022-04-16 11:37:19 + +> An additional problem with compile-time checking is **version skew**. A user +> may have successfully compiled a class, say PurchaseStockOptions, to be a +> subclass of TradingClass. But the definition of TradingClass might have +> changed since the time the class was compiled in a way that is not compatible +> with pre-existing binaries. + +— JVMS8, §4.10 + +> The intent is that a **stack map frame** must appear at the beginning of each +> **basic block** in a method. The stack map frame specifies the verification +> type of each operand stack entry and of each local variable at the start of +> each basic block. + +— JVMS8, §4.10.1 + +### Read + + - Lightweight Bytecode Verification + +## 2022-04-17 14:09:19 + +### Java Bytecode Verification — An Overview + +For every instruction `i`: + +``` +i : in(i) → out(i) +in(i) = lub { out(j) | j predecessor i } +``` + +i₀ = first instruction + +``` +in(i₀) = (ε, (P₀ ... Pₙ₋₁, ⊤ ... ⊤)) +``` + +Pₖ are the types of the parameter methods + +> The dataflow framework presented above requires that the type algebra, +> ordered by the subtyping relation, constitutes a semi-lattice. +— §3.3 + +### Dataflow Analysis [slides] + +> Available expressions is a **forward must** analysis +> +> • **Forward** = Data flow from in to out +> • **Must** = At join points, only keep facts that hold on all paths that are joined + +> Liveness is a **backwards may** analysis +> • To know if a variable is live, we need to look at the future uses of it. We +> propagate facts backwards, from Out to In. +> • Variable is live if it is used on some path From 497d802fb6add1d19acad9e2c9e27e0192ae04ed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 24 Apr 2023 19:07:49 +0300 Subject: [PATCH 30/41] Remove Fn extensions which are now part of sml-foundation --- src/extensions/fn.sig | 9 --------- src/extensions/fn.sml | 6 ------ 2 files changed, 15 deletions(-) delete mode 100644 src/extensions/fn.sig delete mode 100644 src/extensions/fn.sml diff --git a/src/extensions/fn.sig b/src/extensions/fn.sig deleted file mode 100644 index 9b2aae1..0000000 --- a/src/extensions/fn.sig +++ /dev/null @@ -1,9 +0,0 @@ -signature FN = - sig - include FN - - (** - * Like `flip`, but for curried functions. - *) - val swap : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c - end diff --git a/src/extensions/fn.sml b/src/extensions/fn.sml deleted file mode 100644 index f137ab6..0000000 --- a/src/extensions/fn.sml +++ /dev/null @@ -1,6 +0,0 @@ -structure Fn : FN = - struct - open Fn - - fun swap f a b = f b a - end From eb924d423734bb73312cb5e225d08194b7ab44af Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 24 Apr 2023 19:14:07 +0300 Subject: [PATCH 31/41] Add notes about the handling of `_extended` frames --- src/stack-map/stack-map.sml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/stack-map/stack-map.sml b/src/stack-map/stack-map.sml index dd94621..5091097 100644 --- a/src/stack-map/stack-map.sml +++ b/src/stack-map/stack-map.sml @@ -5,6 +5,11 @@ structure StackMap = (* * This frame type indicates that the frame has exactly the same local * variables as the previous frame and that the operand stack is empty. + * + * This entry also handles the `same_frame_extended` case. The distiction + * is based on the `offsetDelta` value. If it's small enough to be + * represented using a `same_frame`, it will use that. Conversely, it + * will use a `same_frame_extended` with an explicit `offset_delta`. *) | Same of { offsetDelta : int } @@ -12,6 +17,11 @@ structure StackMap = * This frame type indicates that the frame has exactly the same local * variables as the previous frame and that the operand stack has one * entry. + * + * This entry also handles the `same_locals_1_stack_item_frame_extended` + * case. Similarly to `same_frame`, the distiction is made based on the + * value of the `offsetDelta` field — if it's too large, then we use the + * extended case. *) | SameLocals1StackItem of { offsetDelta : int, From 0423db78ea20fa4b2f3f2792ee2db066fad181dd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 24 Apr 2023 19:14:50 +0300 Subject: [PATCH 32/41] Leave some reference notes --- src/stack-map/verification-type.sml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/stack-map/verification-type.sml b/src/stack-map/verification-type.sml index a80cd1e..71d29ff 100644 --- a/src/stack-map/verification-type.sml +++ b/src/stack-map/verification-type.sml @@ -2,6 +2,7 @@ structure VerificationType = struct open Util + (* See: JVMS18 / $4.10.1.2 / Verification Type System *) datatype t = Top | Integer @@ -29,6 +30,9 @@ structure VerificationType = | UninitializedThis => "UninitializedThis" | Reference => "Reference" + (** + * See: Java Bytecode Verification — An Overview, p7 + *) fun leastUpperBound a b = case (a, b) of | (Top, _) => Top From f3bb6ba3d454651a57887c17ac4f05311b62b20c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 24 Apr 2023 19:15:40 +0300 Subject: [PATCH 33/41] Add more detail to exception message --- src/stack-map/verification-type.sml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/stack-map/verification-type.sml b/src/stack-map/verification-type.sml index 71d29ff..5472c21 100644 --- a/src/stack-map/verification-type.sml +++ b/src/stack-map/verification-type.sml @@ -40,7 +40,9 @@ structure VerificationType = | (a, b) => if a = b then a - else raise Fail "not implemented: leastUpperBound" (* TODO *) + else + (* TODO *) + raise Fail ("not implemented: leastUpperBound: " ^ toString a ^ " =/= " ^ toString b) fun isTop Top = true | isTop _ = false From 5ec69a2b7fb72726349ed6af5880e96a3fbc7773 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 24 Apr 2023 19:16:55 +0300 Subject: [PATCH 34/41] Support `ireturn` in the bytecode verifier --- src/stack-map/verifier.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/stack-map/verifier.sml b/src/stack-map/verifier.sml index 4d33f17..647ecfd 100644 --- a/src/stack-map/verifier.sml +++ b/src/stack-map/verifier.sml @@ -235,7 +235,7 @@ structure Verifier = | ret index => raise Fail "not implemented: ret" | tableswitch => raise Fail "not implemented: tableswitch" | lookupswitch => raise Fail "not implemented: lookupswitch" - | ireturn => raise Fail "not implemented: ireturn" + | ireturn => [Push VerificationType.Integer] | lreturn => raise Fail "not implemented: lreturn" | freturn => raise Fail "not implemented: freturn" | dreturn => raise Fail "not implemented: dreturn" From 5bef6aa7e5e8dade124ff6d57d3a0769e2c9f22f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 24 Apr 2023 19:24:18 +0300 Subject: [PATCH 35/41] Create directory for test cases and first one: factorial --- dev.cm | 4 + test/test-cases/factorial/Factorial.java | 33 ++++++ test/test-cases/factorial/factorial.sml | 123 +++++++++++++++++++++++ 3 files changed, 160 insertions(+) create mode 100644 test/test-cases/factorial/Factorial.java create mode 100644 test/test-cases/factorial/factorial.sml diff --git a/dev.cm b/dev.cm index 522376e..f395964 100644 --- a/dev.cm +++ b/dev.cm @@ -10,3 +10,7 @@ is all-suites.sml frame-suite.sml ) + + test/test-cases ( + factorial/factorial.sml + ) diff --git a/test/test-cases/factorial/Factorial.java b/test/test-cases/factorial/Factorial.java new file mode 100644 index 0000000..fd9ef8d --- /dev/null +++ b/test/test-cases/factorial/Factorial.java @@ -0,0 +1,33 @@ +/* + +Compile with `-g:none` to forgo all debug symbols: + +``` +$ javac -g:none Factorial.java +``` + +Inspect generated bytecode with: + +``` +$ javap -v Factorial.java +``` + +*/ + +public class Factorial { + public static void main(String[] args) { + int r = factorial(5); + System.out.println(Integer.toString(r)); + } + + public static int factorial(int n) { + int r = 1; + + while (n > 0) { + r = n * r; + n--; + } + + return r; + } +} diff --git a/test/test-cases/factorial/factorial.sml b/test/test-cases/factorial/factorial.sml new file mode 100644 index 0000000..5f80c93 --- /dev/null +++ b/test/test-cases/factorial/factorial.sml @@ -0,0 +1,123 @@ +structure Factorial = + let + val className = "Factorial" + + structure D = Descriptor + structure Instr = LabeledInstr + + val main = Method.from { + name = "main", + accessFlags = [Method.Flag.PUBLIC, Method.Flag.STATIC], + descriptor = Descriptor.Method { + return = Descriptor.Void, + params = [ + Descriptor.Array (Descriptor.Object (ClassName.fromString "java/lang/String")) + ] + }, + attributes = [ + Attr.Code { + exceptionTable = [], + attributes = [], + code = let open Instr in [ + iconst_5, + invokestatic { + class = ClassName.fromString className, + name = "factorial", + descriptor = D.Method { + params = [D.Int], + return = D.Type D.Int + } + }, + istore_1, + getstatic java.lang.System.out, + iload_1, + invokestatic java.lang.Integer.toString, + invokevirtual java.io.PrintStream.println, + return + ] end + } + ] + } + + val factorial = Method.from { + name = "factorial", + accessFlags = [Method.Flag.PUBLIC, Method.Flag.STATIC], + descriptor = Descriptor.Method { + return = Descriptor.Type Descriptor.Int, + params = [ + Descriptor.Int + ] + }, + attributes = [ + Attr.Code { + exceptionTable = [], + attributes = [], + code = let open Instr in [ + iconst_1, + istore_1, + label "enter-while", + iload_0, + ifle "exit-while", + iload_0, + iload_1, + imul, + istore_1, + iinc (0w0, ~ 0w1), + goto "enter-while", + label "exit-while", + iload_1, + ireturn + ] end + } + ] + } + in + struct + fun class name = Class.from { + accessFlags = [Class.Flag.PUBLIC], + thisClass = ClassName.fromString name, + superClass = ClassName.fromString "java/lang/Object", + interfaces = [], + attributes = [Attr.SourceFile "main.sml"], + fields = [ + Field.from { + name = "message", + accessFlags = [Field.Flag.PRIVATE, Field.Flag.STATIC, Field.Flag.FINAL], + descriptor = Descriptor.Field (Descriptor.Object (ClassName.fromString "java/lang/String")), + attributes = [ + Attr.ConstantValue (ConstantValue.String "Hello, World!") + ] + } + ], + methods = [main, factorial] + } + + val trim = + let open Char Substring in + string o dropl isSpace o dropr isSpace o full + end + + fun java { classpath } className = + let + val proc = Unix.execute ("/usr/bin/java", ["-cp", classpath, className]) + val output = TextIO.inputAll (Unix.textInstreamOf proc) + in + Unix.reap proc + ; trim output + end + + fun main () = + let + val workDir = OS.FileSys.getDir () + val binDir = OS.Path.joinDirFile { dir = workDir, file = "bin" } + val fileName = OS.Path.joinDirFile { dir = binDir, file = className ^ ".class" } + val classFile = BinIO.openOut fileName + val bytes = Class.compile (class className) + val _ = BinIO.output (classFile, bytes) + val _ = BinIO.closeOut classFile + val output = java { classpath = binDir } className + in + print (output ^ "\n") + end + end + end From 12e9d939e93fa9ea70ff8b7f1a8aafe2adfd2310 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 20 May 2024 11:22:50 +0300 Subject: [PATCH 36/41] Leave reminder of where I left off work --- log.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/log.md b/log.md index 1b4b2cf..8479d33 100644 --- a/log.md +++ b/log.md @@ -1,5 +1,24 @@ # Work Log +## 2024-05-20 11:19:12 + +https://github.com/GaloisInc/jvm-verifier + +Continue here: + +``` +- CM.make "dev.cm"; Factorial.main (); +[scanning dev.cm] +[scanning $BUCHAREST-ML/sml-test/lib.cm] +[scanning $BUCHAREST-ML/sml-foundation/lib.cm] +[scanning (dev.cm):lib.cm] +[New bindings added.] +val it = true : bool + +uncaught exception Fail [Fail: not implemented: leastUpperBound: Reference =/= Integer] + raised at: src/stack-map/verification-type.sml:47.19-47.98 +``` + ## 2023-04-24 09:56:20 > Each stack map frame described in the entries table relies on the previous From 06b2f047fb3dc85fbef4e68fd250fb41f13950e0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Mon, 20 May 2024 11:23:28 +0300 Subject: [PATCH 37/41] Mass commit in case my laptop bricks again... --- lib/core/lib.cm | 8 +++++ lib/core/src/list.sig | 8 +++++ lib/core/src/list.sml | 31 +++++++++++++++++++ lib/core/src/other.sml | 11 +++++++ src/class-name.sml | 2 +- src/compilable.sig | 33 +++++++++++++++++++++ src/index.sml | 4 +++ src/indexed-instr.sml | 18 +++++++++++ src/main.sml | 46 ++++++++++++++++------------- src/stack-map/stack-lang.sml | 23 ++++++++++----- src/stack-map/stack-map.sml | 10 +++++++ src/stack-map/verification-type.sml | 4 ++- src/stack-map/verifier.sig | 2 +- src/stack-map/verifier.sml | 8 +++-- src/stack-map/verifier2.sml | 28 ++++++++++++++++++ 15 files changed, 203 insertions(+), 33 deletions(-) create mode 100644 lib/core/lib.cm create mode 100644 lib/core/src/list.sig create mode 100644 lib/core/src/list.sml create mode 100644 lib/core/src/other.sml create mode 100644 src/compilable.sig create mode 100644 src/index.sml create mode 100644 src/indexed-instr.sml create mode 100644 src/stack-map/verifier2.sml diff --git a/lib/core/lib.cm b/lib/core/lib.cm new file mode 100644 index 0000000..f779cce --- /dev/null +++ b/lib/core/lib.cm @@ -0,0 +1,8 @@ +library (0.1.0) + signature LIST + structure List +is + $/basis.cm + + src/list.sig + src/list.sml diff --git a/lib/core/src/list.sig b/lib/core/src/list.sig new file mode 100644 index 0000000..f5de07a --- /dev/null +++ b/lib/core/src/list.sig @@ -0,0 +1,8 @@ +signature LIST = + sig + include LIST + + val countWhere : ('a -> bool) -> 'a list -> int + + val foldl : 'a list -> { seed : 'b, step : 'a * 'b -> 'b } -> 'b + end diff --git a/lib/core/src/list.sml b/lib/core/src/list.sml new file mode 100644 index 0000000..e29f872 --- /dev/null +++ b/lib/core/src/list.sml @@ -0,0 +1,31 @@ +structure List : LIST = + struct + open LIST + + fun foldl list { seed, step } = List.foldl step seed list + fun foldr list { seed, step } = List.foldr step seed list + + fun takeWhile _ [] = [] + | takeWhile p (x :: xs) = if p x then x :: takeWhile p xs else [] + + fun takeUntil p = takeWhile (not o p) + + fun countWhere predicate list = + raise Fail "not implemented" + + fun bound xs ys a b = + case (xs, ys) of + (x, []) => a + | ([], y) => b + | (_ :: xs, _ :: ys) => recur xs ys a b + + (** + * Returns the list with more elements. + *) + fun max a b = bound a b a b + + (** + * Returns the list with fewer elements. + *) + fun min a b = bound a b b a + end diff --git a/lib/core/src/other.sml b/lib/core/src/other.sml new file mode 100644 index 0000000..58f79b0 --- /dev/null +++ b/lib/core/src/other.sml @@ -0,0 +1,11 @@ +signature FOLDABLE = + sig + type 'a t + type ('a, 'b) arrow = 'a -> 'b + type 'a monoid = { + zero : 'a, + plus : 'a * 'a -> 'a + } + + val foldMap : 'm monoid -> ('a -> 'm) -> 'a t -> 'm + end diff --git a/src/class-name.sml b/src/class-name.sml index ed62c40..f8eef3e 100644 --- a/src/class-name.sml +++ b/src/class-name.sml @@ -4,6 +4,6 @@ structure ClassName = struct type t = Text.t - fun fromParts parts = Text.concatWith "/" parts + fun fromParts parts = String.concatWith "/" parts fun fromString s = s end diff --git a/src/compilable.sig b/src/compilable.sig new file mode 100644 index 0000000..03cd252 --- /dev/null +++ b/src/compilable.sig @@ -0,0 +1,33 @@ +(* Reader Monad *) +signature CONFIGURABLE = + sig + type 'a t + type config + + val from : (config -> 'a) -> 'a t + + val get : key -> + + val run : config -> 'a t -> 'a + end + +structure Configurable = + struct + type 'computation t = int + + fun from f = + raise Fail "not implemented" + + fun run config = + end + +Configurable.from (fn config => + +) + +signature COMPILABLE = + sig + type t + + val compile : ConstPool.t -> t -> (Word8Vector.vector, ConstPool.t) Configurable.t + end diff --git a/src/index.sml b/src/index.sml new file mode 100644 index 0000000..7f723a8 --- /dev/null +++ b/src/index.sml @@ -0,0 +1,4 @@ +structure Index = + struct + type t = int + end diff --git a/src/indexed-instr.sml b/src/indexed-instr.sml new file mode 100644 index 0000000..34416ec --- /dev/null +++ b/src/indexed-instr.sml @@ -0,0 +1,18 @@ +signature INDEXED_INSTR = + sig + type t + + val index : t -> Index.t + val instr : t -> Instr.t + end + + +structure IndexedInstr : INDEXED_INSTR = + struct + type t = (Index.t, Instr.t) + + val fromPair = Fn.id + + fun index (i, _) => i + fun instr (_, i) => i + end diff --git a/src/main.sml b/src/main.sml index 58430b9..cefba0b 100644 --- a/src/main.sml +++ b/src/main.sml @@ -1,5 +1,7 @@ structure Main = struct + open Fn.Syntax infix |> + structure Instr = LabeledInstr fun symbol class name descriptor = { @@ -272,9 +274,9 @@ structure Main = ] } - val class = Class.from { + fun class name = Class.from { accessFlags = [Class.Flag.PUBLIC], - thisClass = ClassName.fromString "Main", + thisClass = ClassName.fromString name, superClass = ClassName.fromString "java/lang/Object", interfaces = [], attributes = [Attr.SourceFile "main.sml"], @@ -297,9 +299,9 @@ structure Main = string o dropl isSpace o dropr isSpace o full end - fun java classPath className = + fun java { classpath } className = let - val proc = Unix.execute ("/usr/bin/java", ["-cp", classPath, className]) + val proc = Unix.execute ("/usr/bin/java", ["-cp", classpath, className]) val output = TextIO.inputAll (Unix.textInstreamOf proc) in Unix.reap proc @@ -308,27 +310,29 @@ structure Main = fun main () = let + val className = "Main" val workDir = OS.FileSys.getDir () - val bytes = Class.compile class - val f = BinIO.openOut (OS.Path.joinDirFile { dir = workDir, file = "Main.class" }) - val _ = BinIO.output (f, bytes) - val _ = BinIO.closeOut f - val output = java workDir "Main" + val binDir = OS.Path.joinDirFile { dir = workDir, file = "bin" } + val fileName = OS.Path.joinDirFile { dir = binDir, file = className ^ ".class" } + val classFile = BinIO.openOut fileName + val bytes = Class.compile (class className) + val _ = BinIO.output (classFile, bytes) + val _ = BinIO.closeOut classFile + val output = java { classpath = binDir } className in print (output ^ "\n") end fun stackMap () = - let - val { attributes = [Attr.Code { code, ... }], ... } = nestedLoops - val { offsetedInstrs, ... } = Instr.compileList ConstPool.empty code - in - StackLang.compileCompact - ( - StackLang.interpret - ( - Verifier.verify offsetedInstrs - ) - ) - end + case nestedLoops of + | { attributes = [Attr.Code { code, ... }], ... } => + let + val { offsetedInstrs, ... } = Instr.compileList ConstPool.empty code + in + offsetedInstrs + |> Verifier.verify + |> StackLang.interpret + |> StackLang.compileCompact + end + | _ => raise Fail "not implemented" end diff --git a/src/stack-map/stack-lang.sml b/src/stack-map/stack-lang.sml index f29f3df..e2d4d74 100644 --- a/src/stack-map/stack-lang.sml +++ b/src/stack-map/stack-lang.sml @@ -2,12 +2,17 @@ structure StackLang = struct type local_index = int + type indexed_type = { + index : local_index, + vtype : VerificationType.t + } + datatype t = | Push of VerificationType.t | Pop of VerificationType.t - | Load of local_index * VerificationType.t - | Store of local_index * VerificationType.t - | Local of local_index * VerificationType.t + | Load of local_index * VerificationType.t (* indexed_type *) + | Store of local_index * VerificationType.t (* indexed_type *) + | Local of local_index * VerificationType.t (* indexed_type *) | Branch of { targetOffset : int, fallsThrough : bool } exception StackUnderflow @@ -17,11 +22,15 @@ structure StackLang = case t of | Push vtype => "Push " ^ VerificationType.toString vtype | Pop vtype => "Pop " ^ VerificationType.toString vtype - | Load (index, vtype) => "Load ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" - | Store (index, vtype) => "Store ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" - | Local (index, vtype) => "Local ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" + | Load (index, vtype) => + "Load ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" + | Store (index, vtype) => + "Store ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" + | Local (index, vtype) => + "Local ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" | Branch { targetOffset, fallsThrough } => - "Branch { targetOffset = "^ Int.toString targetOffset ^", fallsThrough = "^ Bool.toString fallsThrough ^" }" + "Branch { targetOffset = "^ Int.toString targetOffset + ^", fallsThrough = "^ Bool.toString fallsThrough ^" }" fun interpret instrs = let diff --git a/src/stack-map/stack-map.sml b/src/stack-map/stack-map.sml index 5091097..63fbc42 100644 --- a/src/stack-map/stack-map.sml +++ b/src/stack-map/stack-map.sml @@ -58,6 +58,16 @@ structure StackMap = stack : VerificationType.t list } + (* structure Frame = + struct + type t = frame + + fun toString frame = + case frame of + | Same { offsetDelta } => "Same { "^ Int.toString offsetDelta ^" }" + | + end *) + open Util fun compile constPool frame = diff --git a/src/stack-map/verification-type.sml b/src/stack-map/verification-type.sml index 5472c21..cf20d94 100644 --- a/src/stack-map/verification-type.sml +++ b/src/stack-map/verification-type.sml @@ -4,7 +4,9 @@ structure VerificationType = (* See: JVMS18 / $4.10.1.2 / Verification Type System *) datatype t = - Top + | Top + (* | OneWord *) (* ??? *) + (* | TwoWord *) (* ??? *) | Integer | Float | Long diff --git a/src/stack-map/verifier.sig b/src/stack-map/verifier.sig index 86fb2e1..2436039 100644 --- a/src/stack-map/verifier.sig +++ b/src/stack-map/verifier.sig @@ -1,4 +1,4 @@ signature VERIFIER = sig - val verify : Instr.t list -> StackLang.t list list + val verify : ('offset * Instr.t) list -> { offset : 'offset, instrs : StackLang.t list } list end diff --git a/src/stack-map/verifier.sml b/src/stack-map/verifier.sml index 647ecfd..ad071a7 100644 --- a/src/stack-map/verifier.sml +++ b/src/stack-map/verifier.sml @@ -1,5 +1,5 @@ -structure Verifier = - struct +structure Verifier : VERIFIER = + let open Instr StackLang fun verify instrs = @@ -256,4 +256,8 @@ structure Verifier = { offset = offset, instrs = transition instr }) instrs end + in + struct + val verify = verify + end end diff --git a/src/stack-map/verifier2.sml b/src/stack-map/verifier2.sml new file mode 100644 index 0000000..34e17d6 --- /dev/null +++ b/src/stack-map/verifier2.sml @@ -0,0 +1,28 @@ +(* + * Write it using the final tagless approach? Is it worth it? + *) +(* structure StackLang = + struct + type t = int + end *) + + + +structure Verifier2 : + sig + val verify : Instr.t list -> StackMap.frame list + end + = + struct + fun verify instrs = + let + fun fold (instr, state) = + raise Fail "not implemented" + + val seed = [] + + val r = List.foldl fold seed instrs + in + raise Fail "not implemented" + end + end From 14056073de84930a72183360668fda8bf4a2f549 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Sat, 26 Oct 2024 23:38:27 +0300 Subject: [PATCH 38/41] Working `factorial` with StackMapTable attribute --- readme.md | 4 ++ src/attr.sml | 32 ++++++++++----- src/class.sml | 2 +- src/member.fun | 2 +- src/stack-map/frame.sml | 11 +++++- src/stack-map/stack-lang.sml | 17 ++++---- src/stack-map/stack-map.sml | 7 ++++ src/stack-map/verification-type.sml | 32 +++++++++++++-- src/stack-map/verifier.sml | 38 ++++++++++++------ test/test-cases/factorial/Factorial.java | 2 +- test/test-cases/factorial/factorial.sml | 50 +++++++++++++++++++++--- 11 files changed, 153 insertions(+), 44 deletions(-) diff --git a/readme.md b/readme.md index fb22a19..73488aa 100644 --- a/readme.md +++ b/readme.md @@ -1,5 +1,9 @@ # JVM bytecode assembler in Standard ML +## Similar Projects + + - BiteScript: https://github.com/headius/bitescript + ## Running Main ``` diff --git a/src/attr.sml b/src/attr.sml index 7f53c26..03c80b1 100644 --- a/src/attr.sml +++ b/src/attr.sml @@ -51,9 +51,9 @@ structure Attr = fun isStackMapTable attr = case attr of StackMapTable _ => true | _ => false - fun compile constPool attr = + fun compile constPool attr nameAndType = case attr of - | Code code => compileCode constPool code + | Code code => compileCode constPool code nameAndType | ConstantValue value => compileConstantValue constPool value | Exceptions exceptions => compileExceptions constPool exceptions | Synthetic => compileSynthetic constPool @@ -65,7 +65,7 @@ structure Attr = | attribute => raise Fail "not implemented" (* https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.3 *) - and compileCode constPool { code, exceptionTable, attributes } = + and compileCode constPool { code, exceptionTable, attributes } nameAndType = let fun compileExceptions constPool exceptionTable = (u2 0, constPool) (* TODO: add exceptions *) @@ -83,7 +83,7 @@ structure Attr = seed = { bytes = vec [], length = 0, constPool = constPool }, step = fn (attr, { bytes, length, constPool }) => let - val (attrBytes, constPool) = compile constPool attr + val (attrBytes, constPool) = compile constPool attr nameAndType in { bytes = Word8Vector.concat [bytes, attrBytes], @@ -100,7 +100,9 @@ structure Attr = then (Word8Vector.concat [u2 length, bytes], constPool) else let - val (attrBytes, constPool) = compile constPool stackMapTable + (*) Add the StackMapTable attribute if the caller hasn't + (*) provided one already. + val (attrBytes, constPool) = compile constPool stackMapTable nameAndType val bytes = Word8Vector.concat [bytes, attrBytes] in (Word8Vector.concat [u2 (length + 1), bytes], constPool) @@ -109,7 +111,7 @@ structure Attr = val (attrNameIndex, constPool) = ConstPool.withUtf8 constPool "Code" (* TODO: generate and add StackMapTable only if version >= 50 *) - val (instrBytes, constPool, stackMapAttr) = compileInstructions constPool code + val (instrBytes, constPool, stackMapAttr) = compileInstructions constPool code nameAndType val (exceptionBytes, constPool) = compileExceptions constPool exceptionTable val (attributeBytes, constPool) = compileAttributes constPool stackMapAttr attributes val attributeLength = @@ -127,12 +129,22 @@ structure Attr = (bytes, constPool) end - and compileInstructions constPool code = + and displayVerifierResult result = + let + fun displayStackLangList list = + String.concatWith "; " (List.map StackLang.toString list) + in + List.app (fn { instrs, offset } => Console.println (Int.toString offset ^ ": "^ displayStackLangList instrs)) result + end + + and compileInstructions constPool code nameAndType = let val result = LabeledInstr.compileList constPool code - val stackMapFrames = - StackLang.compileCompact - (StackLang.interpret (Verifier.verify (#offsetedInstrs result))) + val stackLang = Verifier.verify (#offsetedInstrs result) + val () = Console.println "---------------------------------------------" + val () = displayVerifierResult stackLang + val stackMapFrames = StackLang.compileCompact (StackLang.interpret stackLang) + (* val () = List.app (Console.println o StackMap.toString) stackMapFrames *) val stackMapAttr = StackMapTable stackMapFrames val bytes = Word8Vector.concat [ u2 (#maxStack result), diff --git a/src/class.sml b/src/class.sml index 06c912c..a6aded8 100644 --- a/src/class.sml +++ b/src/class.sml @@ -82,7 +82,7 @@ structure Class = if List.null bootstrapMethods then attributes else Attr.BootstrapMethods bootstrapMethods :: attributes - val (attrsBytes, constPool) = compileMany Attr.compile constPool attributes + val (attrsBytes, constPool) = compileMany (fn cp => fn attr => Attr.compile cp attr NONE) constPool attributes val constPoolBytes = ConstPool.compile constPool in Word8Vector.concat [ diff --git a/src/member.fun b/src/member.fun index 2490ec9..4da619c 100644 --- a/src/member.fun +++ b/src/member.fun @@ -25,7 +25,7 @@ functor Member(Flag : sig type t val compile : t -> Word.word end) = fun compileAttrs (attr, (bytes, constPool)) = let - val (attrBytes, constPool) = Attr.compile constPool attr + val (attrBytes, constPool) = Attr.compile constPool attr (SOME { name, descriptor }) in (Word8Vector.concat [bytes, attrBytes], constPool) end diff --git a/src/stack-map/frame.sml b/src/stack-map/frame.sml index 3d2c920..ae6e6e9 100644 --- a/src/stack-map/frame.sml +++ b/src/stack-map/frame.sml @@ -6,17 +6,24 @@ structure Frame = | Chop of int | Append of int + fun toString diff = + case diff of + | Same => "Same" + | Full => "Full" + | Chop n => "Chop " ^ Int.toString n + | Append n => "Append " ^ Int.toString n + fun localsDifference xs ys = let fun chop n xs ys = if n = 3 then case (xs, ys) of - ([], []) => Chop n + | ([], []) => Chop n | _ => Full else case (xs, ys) of - ([], []) => Chop n + | ([], []) => Chop n | (_ :: xs, []) => chop (n + 1) xs [] | (_ :: xs, VerificationType.Top :: ys) => chop (n + 1) xs ys | _ => Full diff --git a/src/stack-map/stack-lang.sml b/src/stack-map/stack-lang.sml index e2d4d74..88c97ef 100644 --- a/src/stack-map/stack-lang.sml +++ b/src/stack-map/stack-lang.sml @@ -22,12 +22,9 @@ structure StackLang = case t of | Push vtype => "Push " ^ VerificationType.toString vtype | Pop vtype => "Pop " ^ VerificationType.toString vtype - | Load (index, vtype) => - "Load ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" - | Store (index, vtype) => - "Store ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" - | Local (index, vtype) => - "Local ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" + | Load (index, vtype) => "Load ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" + | Store (index, vtype) => "Store ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" + | Local (index, vtype) => "Local ("^ Int.toString index ^", "^ VerificationType.toString vtype ^")" | Branch { targetOffset, fallsThrough } => "Branch { targetOffset = "^ Int.toString targetOffset ^", fallsThrough = "^ Bool.toString fallsThrough ^" }" @@ -145,12 +142,14 @@ structure StackLang = val seed = { stack = [], - locals = [VerificationType.Reference, VerificationType.Top, VerificationType.Top], (* TODO *) + locals = [VerificationType.Integer, VerificationType.Top, VerificationType.Top], (* TODO *) frameMap = IntBinaryMap.empty, fallsThrough = true } + + val { frameMap, ... } = List.foldli fold seed instrss in - List.foldli fold seed instrss + IntBinaryMap.listItems frameMap end fun unwrapOffset (index, item) = @@ -162,7 +161,7 @@ structure StackLang = isBranchTarget = isBranchTarget } in - List.mapi unwrapOffset (IntBinaryMap.listItems (#frameMap (eval instrs))) + List.mapi unwrapOffset (eval instrs) end (* TODO: update function *) diff --git a/src/stack-map/stack-map.sml b/src/stack-map/stack-map.sml index 63fbc42..a35b42f 100644 --- a/src/stack-map/stack-map.sml +++ b/src/stack-map/stack-map.sml @@ -68,6 +68,13 @@ structure StackMap = | end *) + fun toString frame = + case frame of + | Same { offsetDelta } => "Same { "^ Int.toString offsetDelta ^" }" + | SameLocals1StackItem { offsetDelta, stack } => + "SameLocals1StackItem { "^ Int.toString offsetDelta ^ ", "^ VerificationType.toString stack ^"}" + | _ => raise Fail "not implemented" + open Util fun compile constPool frame = diff --git a/src/stack-map/verification-type.sml b/src/stack-map/verification-type.sml index cf20d94..8a3f084 100644 --- a/src/stack-map/verification-type.sml +++ b/src/stack-map/verification-type.sml @@ -2,11 +2,37 @@ structure VerificationType = struct open Util - (* See: JVMS18 / $4.10.1.2 / Verification Type System *) + (** + * Verification Type Hierarchy + * + * See: JVMS18 / $4.10.1.2 / Verification Type System + * + * ``` + * top + * ____________/\____________ + * / \ + * / \ + * oneWord twoWord + * / | \ / \ + * / | \ / \ + * int float reference long double + * / \ + * / \_____________ + * / \ + * / \ + * uninitialized +------------------+ + * / \ | Java reference | + * / \ | type hierarchy | + * uninitializedThis uninitialized(Offset) +------------------+ + * | + * | + * null + * ``` + *) datatype t = | Top - (* | OneWord *) (* ??? *) - (* | TwoWord *) (* ??? *) + (* | OneWord *) (* See diagram above *) + (* | TwoWord *) | Integer | Float | Long diff --git a/src/stack-map/verifier.sml b/src/stack-map/verifier.sml index ad071a7..03371e6 100644 --- a/src/stack-map/verifier.sml +++ b/src/stack-map/verifier.sml @@ -2,6 +2,19 @@ structure Verifier : VERIFIER = let open Instr StackLang + (** + * TODO: this function needs to receive the containing methods signature, + * so that we can verify params and return instructions. + * + * For example, `areturn` must verify that the stack contains a reference + * which is a subtype of the declared return type. + * + * > An areturn instruction is type safe iff the enclosing method has a + * > declared return type, ReturnType, that is a reference type, and one + * > can validly pop a type matching ReturnType off the incoming operand + * > stack. + * — JVMS23, p238 + *) fun verify instrs = let fun transition instr = @@ -231,29 +244,32 @@ structure Verifier : VERIFIER = | monitorenter => raise Fail "not implemented: monitorenter" | monitorexit => raise Fail "not implemented: monitorexit" | goto offset => [Branch { targetOffset = offset, fallsThrough = false }] - | jsr offset => raise Fail "not implemented: jsr" - | ret index => raise Fail "not implemented: ret" | tableswitch => raise Fail "not implemented: tableswitch" | lookupswitch => raise Fail "not implemented: lookupswitch" - | ireturn => [Push VerificationType.Integer] - | lreturn => raise Fail "not implemented: lreturn" - | freturn => raise Fail "not implemented: freturn" - | dreturn => raise Fail "not implemented: dreturn" - | areturn => raise Fail "not implemented: areturn" - | return => [Push VerificationType.Top] + | ireturn => [Pop VerificationType.Integer] + | lreturn => [Pop VerificationType.Long] + | freturn => [Pop VerificationType.Float] + | dreturn => [Pop VerificationType.Double] + | areturn => raise Fail "not implemented" + | return => [] | wide => raise Fail "not implemented: wide" | multianewarray _ => raise Fail "not implemented: multianewarray" | ifnull offset => raise Fail "not implemented: ifnull" | ifnonnull offset => raise Fail "not implemented: ifnonnull" | goto_w offset => raise Fail "not implemented: goto_w" - | jsr_w offset => raise Fail "not implemented: jsr_w" | breakpoint => raise Fail "not implemented: breakpoint" | impdep1 => raise Fail "not implemented: impdep1" | impdep2 => raise Fail "not implemented: impdep2" + | ret index => raise Fail "not implemented: ret; disallowed after 50" + | jsr offset => raise Fail "not implemented: jsr; disallowed after 50" + | jsr_w offset => raise Fail "not implemented: jsr; disallowed after 50" in - List.map + Console.println ("VERIFY........"); + List.mapPartial (fn (offset, instr) => - { offset = offset, instrs = transition instr }) + case transition instr of + | [] => NONE + | xs => SOME ({ offset = offset, instrs = xs })) instrs end in diff --git a/test/test-cases/factorial/Factorial.java b/test/test-cases/factorial/Factorial.java index fd9ef8d..cd61031 100644 --- a/test/test-cases/factorial/Factorial.java +++ b/test/test-cases/factorial/Factorial.java @@ -9,7 +9,7 @@ Inspect generated bytecode with: ``` -$ javap -v Factorial.java +$ javap -v Factorial ``` */ diff --git a/test/test-cases/factorial/factorial.sml b/test/test-cases/factorial/factorial.sml index 5f80c93..d7f9733 100644 --- a/test/test-cases/factorial/factorial.sml +++ b/test/test-cases/factorial/factorial.sml @@ -52,26 +52,64 @@ structure Factorial = Attr.Code { exceptionTable = [], attributes = [], + (* + 0: Push Integer + 1: Store (1, Integer) + 2: Load (0, Integer) + 3: Pop Integer; Branch { targetOffset = 10, fallsThrough = true } + 6: Load (0, Integer) + 7: Load (1, Integer) + 8: Pop Integer; Pop Integer; Push Integer + 9: Store (1, Integer) + 10: Local (0, Integer) + 13: Branch { targetOffset = 2, fallsThrough = false } + 16: Load (1, Integer) + 17: Pop Integer + *) code = let open Instr in [ - iconst_1, + iconst_1, (* int r = 1; *) istore_1, - label "enter-while", + label "enter-while", (* while (n > 0) { *) iload_0, ifle "exit-while", - iload_0, + iload_0, (* r = n * r; *) iload_1, imul, istore_1, - iinc (0w0, ~ 0w1), - goto "enter-while", + iinc (0w0, ~ 0w1), (* n-- *) + goto "enter-while", (* } *) label "exit-while", - iload_1, + iload_1, (* return r; *) ireturn ] end } ] } in + (* DSL sketch attempt *) + (* let open Assembly.DSL in + class [PUBLIC] "Factorial" [] [] [ + field [PRIVATE, STATIC, FINAL] "java/lang/String" "Hello, World!" + + method [PUBLIC, STATIC] INT "factorial" [INT] [ + iconst_1, + istore_1, + label "enter-while", + iload_0, + ifle "exit-while", + iload_0, + iload_1, + imul, + istore_1, + iinc (0w0, ~ 0w1), + goto "enter-while", + label "exit-while", + iload_1, + ireturn + ] end + ] + end *) + struct fun class name = Class.from { accessFlags = [Class.Flag.PUBLIC], From a289c581e4fb43f9836a613b6f4eccb36ad23898 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Sun, 27 Oct 2024 00:18:38 +0300 Subject: [PATCH 39/41] Properly initialize locals for verification --- src/attr.sml | 5 +++-- src/descriptor.sml | 2 +- src/main.sml | 19 ++++++++----------- src/method.sml | 3 +++ src/stack-map/stack-lang.sml | 14 ++++++++++++-- 5 files changed, 27 insertions(+), 16 deletions(-) diff --git a/src/attr.sml b/src/attr.sml index 03c80b1..cfeade0 100644 --- a/src/attr.sml +++ b/src/attr.sml @@ -140,15 +140,16 @@ structure Attr = and compileInstructions constPool code nameAndType = let val result = LabeledInstr.compileList constPool code + val maxLocals = #maxLocals result val stackLang = Verifier.verify (#offsetedInstrs result) val () = Console.println "---------------------------------------------" val () = displayVerifierResult stackLang - val stackMapFrames = StackLang.compileCompact (StackLang.interpret stackLang) + val stackMapFrames = StackLang.compileCompact (StackLang.interpret stackLang (Option.valOf nameAndType) maxLocals) (* val () = List.app (Console.println o StackMap.toString) stackMapFrames *) val stackMapAttr = StackMapTable stackMapFrames val bytes = Word8Vector.concat [ u2 (#maxStack result), - u2 (#maxLocals result), + u2 maxLocals, u4 (Word8Vector.length (#bytes result)), (#bytes result) ] diff --git a/src/descriptor.sml b/src/descriptor.sml index 54c93cb..ad12a83 100644 --- a/src/descriptor.sml +++ b/src/descriptor.sml @@ -24,7 +24,7 @@ structure Descriptor = | Void | Type of simple - fun fromString s = Raw s + fun fromString s = Raw s (* ← parse descriptor *) fun paramsCount descriptor = case descriptor of diff --git a/src/main.sml b/src/main.sml index cefba0b..d08c3e3 100644 --- a/src/main.sml +++ b/src/main.sml @@ -324,15 +324,12 @@ structure Main = end fun stackMap () = - case nestedLoops of - | { attributes = [Attr.Code { code, ... }], ... } => - let - val { offsetedInstrs, ... } = Instr.compileList ConstPool.empty code - in - offsetedInstrs - |> Verifier.verify - |> StackLang.interpret - |> StackLang.compileCompact - end - | _ => raise Fail "not implemented" + let + val { offsetedInstrs, maxLocals, ... } = Instr.compileList ConstPool.empty (Method.code nestedLoops) + in + offsetedInstrs + |> Verifier.verify + |> (fn instrs => StackLang.interpret instrs (Method.nameAndType nestedLoops) maxLocals) + |> StackLang.compileCompact + end end diff --git a/src/method.sml b/src/method.sml index 0a5232d..716285c 100644 --- a/src/method.sml +++ b/src/method.sml @@ -33,4 +33,7 @@ structure Method = end structure M = Member(Flag) open M + + fun code ({ attributes = [Attr.Code { code, ... }], ... } : t) = code + | code _ = raise Fail "bug: method without code attribute (abstract method?)" end diff --git a/src/stack-map/stack-lang.sml b/src/stack-map/stack-lang.sml index 88c97ef..3cb3136 100644 --- a/src/stack-map/stack-lang.sml +++ b/src/stack-map/stack-lang.sml @@ -29,7 +29,7 @@ structure StackLang = "Branch { targetOffset = "^ Int.toString targetOffset ^", fallsThrough = "^ Bool.toString fallsThrough ^" }" - fun interpret instrs = + fun interpret instrs { name, descriptor } maxLocals = let fun mergeFrames prev curr = let @@ -140,9 +140,18 @@ structure StackLang = } end + val locals = + let + val args = VerificationType.methodParams descriptor + val nonArgCount = maxLocals - List.length args + val locals = List.tabulate (nonArgCount, fn _ => VerificationType.Top) + in + args @ locals + end + val seed = { stack = [], - locals = [VerificationType.Integer, VerificationType.Top, VerificationType.Top], (* TODO *) + locals = locals, frameMap = IntBinaryMap.empty, fallsThrough = true } @@ -161,6 +170,7 @@ structure StackLang = isBranchTarget = isBranchTarget } in + Console.println ("StackLang: interpreting method: " ^ name ^ ":" ^ Descriptor.compile descriptor); List.mapi unwrapOffset (eval instrs) end From e19f9213fbde1eafd1c32ddca39e830606e4315e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Sun, 27 Oct 2024 00:36:00 +0300 Subject: [PATCH 40/41] Adjust exception message --- src/stack-map/verifier.sml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/stack-map/verifier.sml b/src/stack-map/verifier.sml index 03371e6..86e5c77 100644 --- a/src/stack-map/verifier.sml +++ b/src/stack-map/verifier.sml @@ -260,9 +260,10 @@ structure Verifier : VERIFIER = | breakpoint => raise Fail "not implemented: breakpoint" | impdep1 => raise Fail "not implemented: impdep1" | impdep2 => raise Fail "not implemented: impdep2" - | ret index => raise Fail "not implemented: ret; disallowed after 50" - | jsr offset => raise Fail "not implemented: jsr; disallowed after 50" - | jsr_w offset => raise Fail "not implemented: jsr; disallowed after 50" + + | ret index => raise Fail "Illegal instruction: ret is disallowed. See §4.9.1." + | jsr offset => raise Fail "Illegal instruction: jsr is disallowed. See §4.9.1." + | jsr_w offset => raise Fail "Illegal instruction: jsr_w is disallowed. See §4.9.1." in Console.println ("VERIFY........"); List.mapPartial From b8e79938b8176c0161d24f625d408d8c0631ecfb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ionu=C8=9B=20G=2E=20Stan?= Date: Sun, 27 Oct 2024 00:47:39 +0300 Subject: [PATCH 41/41] Add TODO item --- src/stack-map/stack-lang.sml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/stack-map/stack-lang.sml b/src/stack-map/stack-lang.sml index 3cb3136..62a5680 100644 --- a/src/stack-map/stack-lang.sml +++ b/src/stack-map/stack-lang.sml @@ -90,7 +90,11 @@ structure StackLang = val frame = { stack = stack, locals = locals } val mergedFrame = case IntBinaryMap.find (frameMap, targetOffset) of - NONE => { offset = NONE, frame = frame, isBranchTarget = true } + NONE => { + offset = NONE, (* TODO: use ~1 (negative 1) *) + frame = frame, + isBranchTarget = true + } | SOME { offset, frame = prevFrame, isBranchTarget } => { offset = offset, frame = mergeFrames prevFrame frame,