Merge pull request #1 from ecstasygg/improvements

# Span

Span implements a branch relaxing assembler in Isabelle/HOL, with proofs of termination, minimum layout size and execution correspondence for a bytecode machine with signed 8-bit and 16-bit relative branches

[![](media/demo.gif)](media/demo.mp4)

fun read path =

  let

    val stream = if path = "-" then TextIO.stdIn else TextIO.openIn path

    val text = TextIO.inputN (stream, 1048577)

    val _ = if path = "-" then () else TextIO.closeIn stream

    val fd = if path = "-" then Posix.FileSys.stdin

      else Posix.FileSys.openf (path, Posix.FileSys.O_RDONLY, Posix.FileSys.O.flags [])

    fun close () = if path = "-" then () else Posix.IO.close fd

    fun loop total chunks =

      let

        val bytes = Posix.IO.readVec (fd, Int.min (65536, 1048577 - total))

        val count = Word8Vector.length bytes

      in

        if count = 0 then String.concat (List.rev chunks)

        else if total + count > 1048576 then raise Fail "input exceeds 1 MiB"

        else loop (total + count) (Byte.bytesToString bytes :: chunks)

      end

    val input = loop 0 [] handle exn => ((close () handle _ => ()); raise exn)

    val _ = close ()

  in

    if size text > 1048576 then raise Fail "input exceeds 1 MiB" else text

    input

  end;

fun write path text =

  let

    val stream = BinIO.openOut path

    val _ = BinIO.output (stream, Byte.stringToBytes text)

  in BinIO.closeOut stream end;

    val bytes = Byte.stringToBytes text

    val pid = SysWord.toString (Posix.Process.pidToWord (Posix.ProcEnv.getpid ()))

    val prefix = OS.Path.concat (OS.Path.dir path, "." ^ OS.Path.file path ^ "." ^ pid ^ ".")

    val defaultMode = Posix.FileSys.S.flags [Posix.FileSys.S.irusr, Posix.FileSys.S.iwusr,

      Posix.FileSys.S.irgrp, Posix.FileSys.S.iwgrp, Posix.FileSys.S.iroth, Posix.FileSys.S.iwoth]

    val mode = Posix.FileSys.S.intersect [Posix.FileSys.ST.mode (Posix.FileSys.stat path),

      Posix.FileSys.S.flags [Posix.FileSys.S.irwxu, Posix.FileSys.S.irwxg, Posix.FileSys.S.irwxo]]

      handle exn as OS.SysErr (_, SOME error) =>

        if error = Posix.Error.noent then defaultMode else raise exn

    fun reserve n =

      if n = 128 then raise Fail "cannot reserve output file"

      else

        let

          val temporary = prefix ^ Int.toString n

        in

          (temporary, Posix.FileSys.createf

            (temporary, Posix.FileSys.O_WRONLY, Posix.FileSys.O.excl, mode))

        end handle exn as OS.SysErr (_, SOME error) =>

          if error = Posix.Error.exist then reserve (n + 1) else raise exn

    val (temporary, fd) = reserve 0

    val closed = ref false

    fun close () = (Posix.IO.close fd; closed := true)

    fun discard () =

      ((if !closed then () else close ()) handle _ => ();

       OS.FileSys.remove temporary handle _ => ())

    fun loop offset =

      if offset = Word8Vector.length bytes then ()

      else

        let

          val count = Posix.IO.writeVec (fd, Word8VectorSlice.slice (bytes, offset, NONE))

        in

          if count = 0 then raise Fail "output write made no progress" else loop (offset + count)

        end

  in

    (loop 0; close (); OS.FileSys.rename {old = temporary, new = path})

      handle exn => (discard (); raise exn)

  end;

fun output (ok, message) =

  (TextIO.output (if ok then TextIO.stdOut else TextIO.stdErr, text message);

  | ["disassemble", file] => output (Span.disassemble (chars (read file)))

  | ["assemble", file, "-o", destination] =>

      let

        val input = chars (read file)

        val (ok, bytes) = Span.binary input

        val ((ok, bytes), report) = Span.artifact (chars (read file))

      in

        if ok then

          (write destination (text bytes);

           output (Span.process [chars "assemble"] input))

        else output (false, bytes)

           output (true, report))

        else output (false, report)

      end

  | ["run", file] => output (Span.process (map chars ["run", "4096"]) (chars (read file)))

  | ["run", file, fuel] => output (Span.process (map chars ["run", fuel]) (chars (read file)))

  by (cases op)

    (auto simp: byte_join nat_less_iff div_less_iff_less_mult split: bool.splits if_splits)

theorem decode_canonical:

  "decode bs = Some (op, rest) \<Longrightarrow> encodable op \<and> bs = encode op @ rest"

  by (cases bs)

    (auto simp: nat_less_iff div_less_iff_less_mult mod_less div_eq_0_iff

      nat_add_distrib nat_mult_distrib

      split: if_splits list.splits)

corollary decode_progress:

  "decode bs = Some (op, rest) \<Longrightarrow> length rest < length bs"

  using decode_canonical[of bs op rest]

  by (cases op) (auto split: bool.splits)

theorem encode_injective:

  "encodable a \<Longrightarrow> encodable b \<Longrightarrow> encode a = encode b \<longleftrightarrow> a = b"

  using decode_encode[of a "[]"] decode_encode[of b "[]"]

  by (metis append_Nil option.inject prod.inject)

fun lower :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> nat instruction \<Rightarrow> operation" where

  "lower p W i Nop = Idle"

| "lower p W i Inc = Raise"

definition ordinal :: "char \<Rightarrow> integer" where "ordinal = of_char"

export_code process binary disassemble ascii ordinal in SML module_name Span file_prefix span

export_code process binary artifact disassemble ascii ordinal in SML module_name Span file_prefix span

end

  "bind (Error e) f = Error e"

| "bind (Ok x) f = f x"

lemma bind_assoc: "bind (bind r f) g = bind r (\<lambda>x. bind (f x) g)"

  by (cases r) auto

function decimal :: "nat \<Rightarrow> string" where

  "decimal n = (if n < 10 then [char_of_nat (48 + n)] else decimal (n div 10) @ [char_of_nat (48 + n mod 10)])"

  by pat_completeness auto

| "parse_lines n (s # ss) = bind (parse_line n (words s)) (\<lambda>xs.

    bind (parse_lines (Suc n) ss) (\<lambda>ys. Ok (xs @ ys)))"

fun parse_acc :: "nat \<Rightarrow> string list \<Rightarrow> statement list \<Rightarrow> statement list result" where

  "parse_acc n [] acc = Ok (rev acc)"

| "parse_acc n (s # ss) acc = (case parse_line n (words s) of Error e \<Rightarrow> Error e

    | Ok xs \<Rightarrow> parse_acc (Suc n) ss (rev xs @ acc))"

lemma parse_acc_correct:

  "parse_acc n ss acc = bind (parse_lines n ss) (\<lambda>xs. Ok (rev acc @ xs))"

  by (induction ss arbitrary: n acc) (auto simp: bind_assoc split: result.splits)

declare parse_lines.simps [code drop]

lemma parse_lines_code [code]: "parse_lines n ss = parse_acc n ss []"

  by (cases "parse_lines n ss") (simp_all add: parse_acc_correct)

fun count :: "statement \<Rightarrow> nat" where

  "count (Label l) = 0"

| "count (Emit op) = 1"

    bind (resolve_all env ss) (\<lambda>xs. Ok (x # xs)))"

| "resolve_all env (Pad n # ss) = bind (resolve_all env ss) (\<lambda>xs. Ok (replicate n Nop @ xs))"

fun resolve_acc :: "(string \<times> nat) list \<Rightarrow> statement list \<Rightarrow> nat instruction list \<Rightarrow> nat instruction list result" where

  "resolve_acc env [] acc = Ok (rev acc)"

| "resolve_acc env (Label l # ss) acc = resolve_acc env ss acc"

| "resolve_acc env (Emit op # ss) acc = (case resolve env op of Error e \<Rightarrow> Error e

    | Ok x \<Rightarrow> resolve_acc env ss (x # acc))"

| "resolve_acc env (Pad n # ss) acc = resolve_acc env ss (replicate n Nop @ acc)"

lemma resolve_acc_correct:

  "resolve_acc env ss acc = bind (resolve_all env ss) (\<lambda>xs. Ok (rev acc @ xs))"

proof (induction ss arbitrary: acc)

  case Nil

  then show ?case by simp

next

  case (Cons s ss)

  then show ?case by (cases s) (auto simp: bind_assoc split: result.splits)

qed

declare resolve_all.simps [code drop]

lemma resolve_all_code [code]: "resolve_all env ss = resolve_acc env ss []"

  by (cases "resolve_all env ss") (simp_all add: resolve_acc_correct)

definition source :: "string \<Rightarrow> nat instruction list result" where

  "source s = (if \<not> list_all (\<lambda>c. let n = nat_of_char c in

      n = 9 \<or> n = 10 \<or> n = 13 \<or> (32 \<le> n \<and> n < 127)) s

    case checked p of Error e \<Rightarrow> (False, (if args = [''trace''] then trace p else []) @ e @ newline)

    | Ok bs \<Rightarrow> inspect args p bs)"

definition artifact :: "string \<Rightarrow> (bool \<times> string) \<times> string" where

  "artifact s = (case source s of Error e \<Rightarrow> ((False, e @ newline), e @ newline)

    | Ok p \<Rightarrow> case checked p of Error e \<Rightarrow> ((False, e @ newline), e @ newline)

    | Ok bs \<Rightarrow> ((True, map char_of_nat bs), summary p bs @ hex bs @ newline))"

theorem artifact_binary: "fst (artifact s) = binary s"

  by (auto simp: artifact_def binary_def compile_def split: result.splits)

theorem artifact_report: "(fst (fst (artifact s)), snd (artifact s)) = process [''assemble''] s"

  by (auto simp: artifact_def process_def inspect_def Let_def split: result.splits)

end