Compiler/virtual machine interpreter: Difference between revisions

=={{header|ATS}}==

<lang ats>(*

The Rosetta Code virtual machine task in ATS2 (also known as

Postiats).

Some implementation notes:

* Values are stored as uint32, and it is checked that uint32

really is 32 bits, two’s-complement. Addition and subtraction

are allowed to roll around, and so can be done without casting

to int32. (The C standard specifies that unsigned integer values

will roll around, rather than signal an overflow.)

* Where it matters, the uint32 are stored in little-endian

order. I have *not* optimized the code for x86/AMD64 (which are

little-endian and also can address unaligned data).

* Here I am often writing out code instead of using some library

function. Partly this is to improve code safety (proof at

compile-time that buffers are not overrun, proof of loop

termination, etc.). Partly this is because I do not feel like

using the C library (or ATS interfaces to it) all that much.

* I am using linear types and so forth, because I think it

interesting to do so. It is unnecessary to use a garbage

collector, because there are no memory leaks. (Not that we

couldn’t simply let memory leak, for this little program with no

REPL.)

*)

#define ATS_EXTERN_PREFIX "rosettacode_vm_"

#define ATS_DYNLOADFLAG 0 (* No initialization is needed. *)

#include "share/atspre_define.hats"

#include "share/atspre_staload.hats"

staload UN = "prelude/SATS/unsafe.sats"

#define NIL list_vt_nil ()

#define :: list_vt_cons

(* The stack has a fixed size but is very large. (Alternatively, one

could make the stack double in size whenever it overflows. Design

options such as using a linked list for the stack come with a

performance penalty.) *)

#define VMSTACK_SIZE 65536

macdef vmstack_size = (i2sz VMSTACK_SIZE)

(* In this program, exceptions are not meant to be caught, unless

the catcher terminates the program. Linear types and

general exception-catching do not go together well. *)

exception bad_vm of string

exception vm_runtime_error of string

(********************************************************************)

(* *)

(* Some string functions that are safe against buffer overruns. *)

(* *)

fn

skip_whitespace {n, i : int | 0 <= i; i <= n}

(s : string n,

n : size_t n,

i : size_t i) :

[j : int | i <= j; j <= n]

size_t j =

let

fun

loop {k : int | i <= k; k <= n} .<n - k>.

(k : size_t k) :

[j : int | i <= j; j <= n]

size_t j =

if k = n then

k

else if isspace (s[k]) then

loop (succ k)

else

k

in

loop (i)

end

fn

skip_non_whitespace {n, i : int | 0 <= i; i <= n}

(s : string n,

n : size_t n,

i : size_t i) :

[j : int | i <= j; j <= n]

size_t j =

let

fun

loop {k : int | i <= k; k <= n} .<n - k>.

(k : size_t k) :

[j : int | i <= j; j <= n]

size_t j =

if k = n then

k

else if isspace (s[k]) then

k

else

loop (succ k)

in

loop (i)

end

fn

substr_equal {n, i, j : int | 0 <= i; i <= j; j <= n}

{m : int | 0 <= m}

(s : string n,

i : size_t i,

j : size_t j,

t : string m) : bool =

(* Is s[i .. j-1] equal to t? *)

let

val m = string_length t

in

if m <> j - i then

false

else

let

fun

loop {k : int | 0 <= k; k <= m} .<m - k>.

(k : size_t k) : bool =

if k = m then

true

else if s[i + k] <> t[k] then

false

else

loop (succ k)

in

loop (i2sz 0)

end

end

(********************************************************************)

(* *)

(* vmint = 32-bit two’s-complement numbers. *)

(* *)

stadef vmint_kind = uint32_kind

typedef vmint = uint32

extern castfn i2vm : int -<> vmint

extern castfn u2vm : uint -<> vmint

extern castfn byte2vm : byte -<> vmint

extern castfn vm2i : vmint -<> int

extern castfn vm2sz : vmint -<> size_t

extern castfn vm2byte : vmint -<> byte

%{^

/*

* The ATS prelude might not have C implementations of all the

* operations we would like to have, so here are some.

*/

typedef uint32_t vmint_t;

ATSinline() vmint_t

rosettacode_vm_g0uint_add_vmint (vmint_t x, vmint_t y)

{

return (x + y);

}

ATSinline() vmint_t

rosettacode_vm_g0uint_sub_vmint (vmint_t x, vmint_t y)

{

return (x - y);

}

ATSinline() int

rosettacode_vm_g0uint_eq_vmint (vmint_t x, vmint_t y)

{

return (x == y);

}

typedef uint32_t vmint_t;

ATSinline() int

rosettacode_vm_g0uint_neq_vmint (vmint_t x, vmint_t y)

{

return (x != y);

}

ATSinline() vmint_t

rosettacode_vm_g0uint_equality_vmint (vmint_t x, vmint_t y)

{

return (vmint_t) (x == y);

}

ATSinline() vmint_t

rosettacode_vm_g0uint_inequality_vmint (vmint_t x, vmint_t y)

{

return (vmint_t) (x != y);

}

ATSinline() vmint_t

rosettacode_vm_g0uint_signed_lt_vmint (vmint_t x, vmint_t y)

{

return (vmint_t) ((int32_t) x < (int32_t) y);

}

ATSinline() vmint_t

rosettacode_vm_g0uint_signed_gt_vmint (vmint_t x, vmint_t y)

{

return (vmint_t) ((int32_t) x > (int32_t) y);

}

ATSinline() vmint_t

rosettacode_vm_g0uint_signed_lte_vmint (vmint_t x, vmint_t y)

{

return (vmint_t) ((int32_t) x <= (int32_t) y);

}

ATSinline() vmint_t

rosettacode_vm_g0uint_signed_gte_vmint (vmint_t x, vmint_t y)

{

return (vmint_t) ((int32_t) x >= (int32_t) y);

}

ATSinline() vmint_t

rosettacode_vm_g0uint_signed_mul_vmint (vmint_t x, vmint_t y)

{

return (vmint_t) ((int32_t) x * (int32_t) y);

}

ATSinline() vmint_t

rosettacode_vm_g0uint_signed_div_vmint (vmint_t x, vmint_t y)

{

return (vmint_t) ((int32_t) x / (int32_t) y);

}

ATSinline() vmint_t

rosettacode_vm_g0uint_signed_mod_vmint (vmint_t x, vmint_t y)

{

return (vmint_t) ((int32_t) x % (int32_t) y);

}

ATSinline() vmint_t

rosettacode_vm_g0uint_logical_not_vmint (vmint_t x)

{

return (vmint_t) (!x);

}

ATSinline() vmint_t

rosettacode_vm_g0uint_logical_and_vmint (vmint_t x, vmint_t y)

{

return (vmint_t) ((!!x) * (!!y));

}

ATSinline() vmint_t

rosettacode_vm_g0uint_logical_or_vmint (vmint_t x, vmint_t y)

{

return (vmint_t) (1 - ((!x) * (!y)));

}

%}

extern fn g0uint_add_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

extern fn g0uint_sub_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

extern fn g0uint_eq_vmint (x : vmint, y : vmint) :<> bool = "mac#%"

extern fn g0uint_neq_vmint (x : vmint, y : vmint) :<> bool = "mac#%"

implement g0uint_add<vmint_kind> (x, y) = g0uint_add_vmint (x, y)

implement g0uint_sub<vmint_kind> (x, y) = g0uint_sub_vmint (x, y)

implement g0uint_eq<vmint_kind> (x, y) = g0uint_eq_vmint (x, y)

implement g0uint_neq<vmint_kind> (x, y) = g0uint_neq_vmint (x, y)

extern fn

g0uint_signed_mul_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

extern fn

g0uint_signed_div_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

extern fn

g0uint_signed_mod_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

extern fn

g0uint_equality_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

extern fn

g0uint_inequality_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

extern fn

g0uint_signed_lt_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

extern fn

g0uint_signed_gt_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

extern fn

g0uint_signed_lte_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

extern fn

g0uint_signed_gte_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

extern fn

g0uint_logical_not_vmint (x : vmint) :<> vmint = "mac#%"

extern fn

g0uint_logical_and_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

extern fn

g0uint_logical_or_vmint (x : vmint, y : vmint) :<> vmint = "mac#%"

overload signed_mul with g0uint_signed_mul_vmint

overload signed_div with g0uint_signed_div_vmint

overload signed_mod with g0uint_signed_mod_vmint

overload equality with g0uint_equality_vmint

overload inequality with g0uint_inequality_vmint

overload signed_lt with g0uint_signed_lt_vmint

overload signed_gt with g0uint_signed_gt_vmint

overload signed_lte with g0uint_signed_lte_vmint

overload signed_gte with g0uint_signed_gte_vmint

overload logical_not with g0uint_logical_not_vmint

overload logical_and with g0uint_logical_and_vmint

overload logical_or with g0uint_logical_or_vmint

fn {}

twos_complement (x : vmint) :<>

vmint =

(~x) + i2vm 1

fn

ensure_that_vmint_is_suitable () : void =

{

val _ = assertloc (u2vm (0xFFFFFFFFU) + u2vm 1U = u2vm 0U)

val _ = assertloc (u2vm 0U - u2vm 1U = u2vm (0xFFFFFFFFU))

val _ = assertloc (i2vm (~1234) = twos_complement (i2vm 1234))

}

fn

parse_digits {n, i, j : int | 0 <= i; i <= j; j <= n}

(s : string n,

i : size_t i,

j : size_t j) :

vmint =

let

val bad_integer = "Bad integer."

fun

loop {k : int | i <= k; k <= j} .<j - k>.

(k : size_t k,

x : vmint) : vmint =

if k = j then

x

else if ~isdigit (s[k]) then

$raise bad_vm (bad_integer)

else

(* The result is allowed to overflow freely. *)

loop (succ k, (i2vm 10 * x) + i2vm (char2i s[k] - char2i '0'))

in

if j = i then

$raise bad_vm (bad_integer)

else

loop (i, i2vm 0)

end

fn

parse_integer {n, i, j : int | 0 <= i; i <= j; j <= n}

(s : string n,

i : size_t i,

j : size_t j) :

vmint =

let

val bad_integer = "Bad integer."

in

if j = i then

$raise bad_vm (bad_integer)

else if j = succ i && ~isdigit (s[i]) then

$raise bad_vm (bad_integer)

else if s[i] <> '-' then

parse_digits (s, i, j)

else if succ i = j then

$raise bad_vm (bad_integer)

else

twos_complement (parse_digits (s, succ i, j))

end

(********************************************************************)

(* *)

(* A linear array type for elements of vmint, byte, etc. *)

(* *)

vtypedef vmarray_vt (t : t@ype+, n : int, p : addr) =

@{

pf = @[t][n] @ p,

pfgc = mfree_gc_v p |

n = size_t n,

p = ptr p

}

vtypedef vmarray_vt (t : t@ype+, n : int) =

[p : addr] vmarray_vt (t, n, p)

fn {t : t@ype}

vmarray_vt_alloc {n : int}

(n : size_t n,

fill : t) :

[p : addr | null < p]

vmarray_vt (t, n, p) =

let

val @(pf, pfgc | p) = array_ptr_alloc<t> (n)

val _ = array_initize_elt (!p, n, fill)

in

@{

pf = pf,

pfgc = pfgc |

n = n,

p = p

}

end

fn {t : t@ype}

vmarray_vt_free {n : int}

{p : addr}

(arr : vmarray_vt (t, n, p)) :

void =

let

val @{

pf = pf,

pfgc = pfgc |

n = n,

p = p

} = arr

in

array_ptr_free (pf, pfgc | p)

end

fn {t : t@ype}

vmarray_vt_fill {n : int}

{p : addr}

(arr : !vmarray_vt (t, n, p),

fill : t) :

void =

array_initize_elt (!(arr.p), (arr.n), fill)

fn {t : t@ype}

{tk : tkind}

vmarray_vt_get_at_g1int {n, i : int | 0 <= i; i < n}

(arr : !vmarray_vt (t, n),

i : g1int (tk, i)) :

t =

array_get_at (!(arr.p), i)

fn {t : t@ype}

{tk : tkind}

vmarray_vt_get_at_g1uint {n, i : int | 0 <= i; i < n}

(arr : !vmarray_vt (t, n),

i : g1uint (tk, i)) :

t =

array_get_at (!(arr.p), i)

overload [] with vmarray_vt_get_at_g1int

overload [] with vmarray_vt_get_at_g1uint

fn {t : t@ype}

{tk : tkind}

vmarray_vt_set_at_g1int {n, i : int | 0 <= i; i < n}

(arr : !vmarray_vt (t, n),

i : g1int (tk, i),

x : t) :

void =

array_set_at (!(arr.p), i, x)

fn {t : t@ype}

{tk : tkind}

vmarray_vt_set_at_g1uint {n, i : int | 0 <= i; i < n}

(arr : !vmarray_vt (t, n),

i : g1uint (tk, i),

x : t) :

void =

array_set_at (!(arr.p), i, x)

overload [] with vmarray_vt_set_at_g1int

overload [] with vmarray_vt_set_at_g1uint

fn {t : t@ype}

vmarray_vt_length {n : int}

(arr : !vmarray_vt (t, n)) :<>

size_t n =

arr.n

(********************************************************************)

(* *)

(* Storage for the strings section. *)

(* *)

vtypedef vmstring_vt (n : int, p : addr) =

@{

(* A vmstring_vt is NUL-terminated, and thus there is [n + 1]

instead of [n] in the following declaration. *)

pf = @[char][n + 1] @ p,

pfgc = mfree_gc_v p |

length = size_t n,

p = ptr p

}

vtypedef vmstring_vt (n : int) = [p : addr] vmstring_vt (n, p)

vtypedef vmstring_vt = [n : int | 0 <= n] vmstring_vt (n)

vtypedef vmstrings_section_vt (n : int, p : addr) =

@{

pf = @[vmstring_vt][n] @ p,

pfgc = mfree_gc_v p |

n = size_t n,

p = ptr p

}

vtypedef vmstrings_section_vt (n : int) =

[p : addr] vmstrings_section_vt (n, p)

fn {t : t@ype}

vmstrings_section_vt_length {n : int}

(arr : !vmstrings_section_vt (n)) :<>

size_t n =

arr.n

fn

vmstring_vt_free {n : int}

{p : addr}

(s : vmstring_vt (n, p)) :

void =

array_ptr_free (s.pf, s.pfgc | s.p)

fn

vmstrings_section_vt_free {n : int}

{p : addr}

(strings : vmstrings_section_vt (n, p)) :

void =

{

fun

free_the_strings {n : int | 0 <= n}

{p : addr} .<n>.

(pf : !(@[vmstring_vt][n] @ p) >>

@[vmstring_vt?][n] @ p |

n : size_t n,

p : ptr p) : void =

if n = 0 then

{

prval _ = pf :=

array_v_unnil_nil {vmstring_vt, vmstring_vt?} pf

}

else

{

prval @(pf_element, pf_rest) = array_v_uncons pf

val _ = vmstring_vt_free (!p)

val p_next = ptr_succ<vmstring_vt> (p)

val _ = free_the_strings (pf_rest | pred n, p_next)

prval _ = pf := array_v_cons (pf_element, pf_rest)

}

val @{

pf = pf,

pfgc = pfgc |

n = n,

p = p

} = strings

prval _ = lemma_g1uint_param n

val _ = free_the_strings (pf | n, p)

val _ = array_ptr_free (pf, pfgc | p)

}

fn

quoted_string_length {n : int | 0 <= n}

(s : string n,

n : size_t n) :

[m : int | 0 <= m; m <= n - 2]

size_t m =

let

val bad_quoted_string = "Bad quoted string."

fun

loop {i : int | 1 <= i; i <= n - 1}

{j : int | 0 <= j; j <= i - 1} .<n - i>.

(i : size_t i,

j : size_t j) :

[k : int | 0 <= k; k <= n - 2]

size_t k =

if i = pred n then

j

else if s[i] <> '\\' then

loop (succ i, succ j)

else if succ i = pred n then

$raise bad_vm (bad_quoted_string)

else if s[succ i] = 'n' || s[succ i] = '\\' then

loop (succ (succ i), succ j)

else

$raise bad_vm (bad_quoted_string)

in

if n < i2sz 2 then

$raise bad_vm (bad_quoted_string)

else if s[0] <> '"' then

$raise bad_vm (bad_quoted_string)

else if s[pred n] <> '"' then

$raise bad_vm (bad_quoted_string)

else

loop (i2sz 1, i2sz 0)

end

fn

dequote_string {m, n : int | 0 <= m; m <= n - 2}

(s : string n,

n : size_t n,

t : !vmstring_vt m) :

void =

let

fun

loop {i : int | 1 <= i; i <= n - 1}

{j : int | 0 <= j; j <= i - 1} .<n - i>.

(t : !vmstring_vt m,

i : size_t i,

j : size_t j) : void =

let

macdef t_str = !(t.p)

in

if i = pred n then

()

else if (t.length) < j then

assertloc (false)

else if s[i] <> '\\' then

begin

t_str[j] := s[i];

loop (t, succ i, succ j)

end

else if succ i = pred n then

assertloc (false)

else if s[succ i] = 'n' then

begin

t_str[j] := '\n';

loop (t, succ (succ i), succ j)

end

else

begin

t_str[j] := s[succ i];

loop (t, succ (succ i), succ j)

end

end

in

loop (t, i2sz 1, i2sz 0)

end

fn

read_vmstrings {strings_size : int}

{strings_addr : addr}

(pf_strings :

!(@[vmstring_vt?][strings_size] @ strings_addr) >>

@[vmstring_vt][strings_size] @ strings_addr |

f : FILEref,

strings_size : size_t strings_size,

strings : ptr strings_addr) :

void =

let

prval _ = lemma_g1uint_param strings_size

fun

loop {k : int | 0 <= k; k <= strings_size} .<strings_size - k>.

(lst : list_vt (vmstring_vt, k),

k : size_t k) :

list_vt (vmstring_vt, strings_size) =

if k = strings_size then

list_vt_reverse (lst)

else

let

val bad_quoted_string = "Bad quoted string."

val line = fileref_get_line_string (f)

val s = $UN.strptr2string (line)

val n = string_length s

val str_length = quoted_string_length (s, n)

val (pf, pfgc | p) =

array_ptr_alloc<char> (succ str_length)

val _ = array_initize_elt (!p, succ str_length, '\0')

val vmstring =

@{

pf = pf,

pfgc = pfgc |

length = str_length,

p = p

}

in

dequote_string (s, n, vmstring);

free line;

loop (vmstring :: lst, succ k)

end

val lst = loop (NIL, i2sz 0)

in

array_initize_list_vt<vmstring_vt>

(!strings, sz2i strings_size, lst)

end

fn

vmstrings_section_vt_read {strings_size : int}

(f : FILEref,

strings_size : size_t strings_size) :

[p : addr]

vmstrings_section_vt (strings_size, p) =

let

val @(pf, pfgc | p) = array_ptr_alloc<vmstring_vt> strings_size

val _ = read_vmstrings (pf | f, strings_size, p)

in

@{

pf = pf,

pfgc = pfgc |

n = strings_size,

p = p

}

end

fn

vmstring_fprint {n, i : int | i < n}

(f : FILEref,

strings : !vmstrings_section_vt n,

i : size_t i) :

void =

{

(*

* The following code does some ‘unsafe’ tricks. For instance, it

* is assumed each stored string is NUL-terminated.

*)

fn

print_it (str : !vmstring_vt) : void =

fileref_puts (f, $UN.cast{string} (str.p))

prval _ = lemma_g1uint_param i

val p_element = array_getref_at (!(strings.p), i)

val @(pf_element | p_element) =

$UN.castvwtp0

{[n : int; p : addr] @(vmstring_vt @ p | ptr p)}

(p_element)

val _ = print_it (!p_element)

prval _ = $UN.castview0{void} pf_element

}

(********************************************************************)

(* *)

(* vm_vt: the dataviewtype for a virtual machine. *)

(* *)

datatype instruction_t =

| instruction_t_1 of (byte)

| instruction_t_5 of (byte, byte, byte, byte, byte)

#define OPCODE_COUNT 24

#define OP_HALT 0x0000 // 00000

#define OP_ADD 0x0001 // 00001

#define OP_SUB 0x0002 // 00010

#define OP_MUL 0x0003 // 00011

#define OP_DIV 0x0004 // 00100

#define OP_MOD 0x0005 // 00101

#define OP_LT 0x0006 // 00110

#define OP_GT 0x0007 // 00111

#define OP_LE 0x0008 // 01000

#define OP_GE 0x0009 // 01001

#define OP_EQ 0x000A // 01010

#define OP_NE 0x000B // 01011

#define OP_AND 0x000C // 01100

#define OP_OR 0x000D // 01101

#define OP_NEG 0x000E // 01110

#define OP_NOT 0x000F // 01111

#define OP_PRTC 0x0010 // 10000

#define OP_PRTI 0x0011 // 10001

#define OP_PRTS 0x0012 // 10010

#define OP_FETCH 0x0013 // 10011

#define OP_STORE 0x0014 // 10100

#define OP_PUSH 0x0015 // 10101

#define OP_JMP 0x0016 // 10110

#define OP_JZ 0x0017 // 10111

#define REGISTER_PC 0

#define REGISTER_SP 1

#define MAX_REGISTER REGISTER_SP

vtypedef vm_vt (strings_size : int,

strings_addr : addr,

code_size : int,

code_addr : addr,

data_size : int,

data_addr : addr,

stack_size : int,

stack_addr : addr) =

@{

strings = vmstrings_section_vt (strings_size, strings_addr),

code = vmarray_vt (byte, code_size, code_addr),

data = vmarray_vt (vmint, data_size, data_addr),

stack = vmarray_vt (vmint, stack_size, stack_addr),

registers = vmarray_vt (vmint, MAX_REGISTER + 1)

}

vtypedef vm_vt (strings_size : int,

code_size : int,

data_size : int,

stack_size : int) =

[strings_addr : addr]

[code_addr : addr]

[data_addr : addr]

[stack_addr : addr]

vm_vt (strings_size, strings_addr,

code_size, code_addr,

data_size, data_addr,

stack_size, stack_addr)

vtypedef vm_vt =

[strings_size : int]

[code_size : int]

[data_size : int]

[stack_size : int]

vm_vt (strings_size, code_size, data_size, stack_size)

fn

vm_vt_free (vm : vm_vt) :

void =

let

val @{

strings = strings,

code = code,

data = data,

stack = stack,

registers = registers

} = vm

in

vmstrings_section_vt_free strings;

vmarray_vt_free<byte> code;

vmarray_vt_free<vmint> data;

vmarray_vt_free<vmint> stack;

vmarray_vt_free<vmint> registers

end

fn

opcode_name_to_byte {n, i, j : int | 0 <= i; i <= j; j <= n}

(arr : &(@[String0][OPCODE_COUNT]),

str : string n,

i : size_t i,

j : size_t j) :

byte =

let

fun

loop {k : int | 0 <= k; k <= OPCODE_COUNT} .<OPCODE_COUNT - k>.

(arr : &(@[String0][OPCODE_COUNT]),

k : int k) : byte =

if k = OPCODE_COUNT then

$raise bad_vm ("Unrecognized opcode name.")

else if substr_equal (str, i, j, arr[k]) then

i2byte k

else

loop (arr, succ k)

in

loop (arr, 0)

end

fn {}

vmint_byte0 (i : vmint) :<>

byte =

vm2byte (i land (u2vm 0xFFU))

fn {}

vmint_byte1 (i : vmint) :<>

byte =

vm2byte ((i >> 8) land (u2vm 0xFFU))

fn {}

vmint_byte2 (i : vmint) :<>

byte =

vm2byte ((i >> 16) land (u2vm 0xFFU))

fn {}

vmint_byte3 (i : vmint) :<>

byte =

vm2byte (i >> 24)

fn

parse_instruction {n : int | 0 <= n}

(arr : &(@[String0][OPCODE_COUNT]),

line : string n) :

instruction_t =

let

val bad_instruction = "Bad VM instruction."

val n = string_length (line)

val i = skip_whitespace (line, n, i2sz 0)

(* Skip the address field*)

val i = skip_non_whitespace (line, n, i)

val i = skip_whitespace (line, n, i)

val j = skip_non_whitespace (line, n, i)

val opcode = opcode_name_to_byte (arr, line, i, j)

val start_of_argument = j

fn

finish_push () :

instruction_t =

let

val i1 = skip_whitespace (line, n, start_of_argument)

val j1 = skip_non_whitespace (line, n, i1)

val arg = parse_integer (line, i1, j1)

in

(* Little-endian storage. *)

instruction_t_5 (opcode, vmint_byte0 arg, vmint_byte1 arg,

vmint_byte2 arg, vmint_byte3 arg)

end

fn

finish_fetch_or_store () :

instruction_t =

let

val i1 = skip_whitespace (line, n, start_of_argument)

val j1 = skip_non_whitespace (line, n, i1)

in

if j1 - i1 < i2sz 3 then

$raise bad_vm (bad_instruction)

else if line[i1] <> '\[' || line[pred j1] <> ']' then

$raise bad_vm (bad_instruction)

else

let

val arg = parse_integer (line, succ i1, pred j1)

in

(* Little-endian storage. *)

instruction_t_5 (opcode, vmint_byte0 arg, vmint_byte1 arg,

vmint_byte2 arg, vmint_byte3 arg)

end

end

fn

finish_jmp_or_jz () :

instruction_t =

let

val i1 = skip_whitespace (line, n, start_of_argument)

val j1 = skip_non_whitespace (line, n, i1)

in

if j1 - i1 < i2sz 3 then

$raise bad_vm (bad_instruction)

else if line[i1] <> '\(' || line[pred j1] <> ')' then

$raise bad_vm (bad_instruction)

else

let

val arg = parse_integer (line, succ i1, pred j1)

in

(* Little-endian storage. *)

instruction_t_5 (opcode, vmint_byte0 arg, vmint_byte1 arg,

vmint_byte2 arg, vmint_byte3 arg)

end

end

in

case+ byte2int0 opcode of

| OP_PUSH => finish_push ()

| OP_FETCH => finish_fetch_or_store ()

| OP_STORE => finish_fetch_or_store ()

| OP_JMP => finish_jmp_or_jz ()

| OP_JZ => finish_jmp_or_jz ()

| _ => instruction_t_1 (opcode)

end

fn

read_instructions (f : FILEref,

arr : &(@[String0][OPCODE_COUNT])) :

(List_vt (instruction_t), Size_t) =

(* Read the instructions from the input, producing a list of

instruction_t objects, and also calculating the total

number of bytes in the instructions. *)

let

fun

loop (arr : &(@[String0][OPCODE_COUNT]),

lst : List_vt (instruction_t),

bytes_needed : Size_t) :

@(List_vt (instruction_t), Size_t) =

if fileref_is_eof f then

@(list_vt_reverse lst, bytes_needed)

else

let

val line = fileref_get_line_string (f)

in

if fileref_is_eof f then

begin

free line;

@(list_vt_reverse lst, bytes_needed)

end

else

let

val instruction =

parse_instruction (arr, $UN.strptr2string line)

val _ = free line

prval _ = lemma_list_vt_param lst

in

case+ instruction of

| instruction_t_1 _ =>

loop (arr, instruction :: lst, bytes_needed + i2sz 1)

| instruction_t_5 _ =>

loop (arr, instruction :: lst, bytes_needed + i2sz 5)

end

end

in

loop (arr, NIL, i2sz 0)

end

fn

list_of_instructions_to_code {bytes_needed : int}

(lst : List_vt (instruction_t),

bytes_needed : size_t bytes_needed) :

[bytes_needed : int]

vmarray_vt (byte, bytes_needed) =

(* This routine consumes and destroys lst. *)

let

fun

loop {n : int | 0 <= n} .<n>.

(code : &vmarray_vt (byte, bytes_needed),

lst : list_vt (instruction_t, n),

i : Size_t) : void =

case+ lst of

| ~ NIL => ()

| ~ (instruction_t_1 (byte1) :: tail) =>

let

val _ = assertloc (i < bytes_needed)

in

code[i] := byte1;

loop (code, tail, i + i2sz 1)

end

| ~ (instruction_t_5 (byte1, byte2, byte3, byte4, byte5)

:: tail) =>

let

val _ = assertloc (i + i2sz 4 < bytes_needed)

in

code[i] := byte1;

code[i + i2sz 1] := byte2;

code[i + i2sz 2] := byte3;

code[i + i2sz 3] := byte4;

code[i + i2sz 4] := byte5;

loop (code, tail, i + i2sz 5)

end

var code = vmarray_vt_alloc<byte> (bytes_needed, i2byte OP_HALT)

prval _ = lemma_list_vt_param lst

prval _ = lemma_g1uint_param bytes_needed

val _ = loop (code, lst, i2sz 0)

in

code

end

fn

read_and_parse_code (f : FILEref,

arr : &(@[String0][OPCODE_COUNT])) :

[bytes_needed : int]

vmarray_vt (byte, bytes_needed) =

let

val @(instructions, bytes_needed) = read_instructions (f, arr)

in

list_of_instructions_to_code (instructions, bytes_needed)

end

fn

parse_header_line {n : int | 0 <= n}

(line : string n) :

@(vmint, vmint) =

let

val bad_vm_header_line = "Bad VM header line."

val n = string_length (line)

val i = skip_whitespace (line, n, i2sz 0)

val j = skip_non_whitespace (line, n, i)

val _ = if ~substr_equal (line, i, j, "Datasize:") then

$raise bad_vm (bad_vm_header_line)

val i = skip_whitespace (line, n, j)

val j = skip_non_whitespace (line, n, i)

val data_size = parse_integer (line, i, j)

val i = skip_whitespace (line, n, j)

val j = skip_non_whitespace (line, n, i)

val _ = if ~substr_equal (line, i, j, "Strings:") then

$raise bad_vm (bad_vm_header_line)

val i = skip_whitespace (line, n, j)

val j = skip_non_whitespace (line, n, i)

val strings_size = parse_integer (line, i, j)

in

@(data_size, strings_size)

end

fn

read_vm (f : FILEref,

opcode_names_arr : &(@[String0][OPCODE_COUNT])) :

vm_vt =

let

val line = fileref_get_line_string (f)

val @(data_size, strings_size) =

parse_header_line ($UN.strptr2string line)

val _ = free line

val [data_size : int] data_size =

g1ofg0 (vm2sz data_size)

val [strings_size : int] strings_size =

g1ofg0 (vm2sz strings_size)

prval _ = lemma_g1uint_param data_size

prval _ = lemma_g1uint_param strings_size

prval _ = prop_verify {0 <= data_size} ()

prval _ = prop_verify {0 <= strings_size} ()

val strings = vmstrings_section_vt_read (f, strings_size)

val code = read_and_parse_code (f, opcode_names_arr)

val data = vmarray_vt_alloc<vmint> (data_size, i2vm 0)

val stack = vmarray_vt_alloc<vmint> (vmstack_size, i2vm 0)

val registers = vmarray_vt_alloc<vmint> (i2sz (MAX_REGISTER + 1),

i2vm 0)

in

@{

strings = strings,

code = code,

data = data,

stack = stack,

registers = registers

}

end

fn {}

pop (vm : &vm_vt) :

vmint =

let

macdef registers = vm.registers

macdef stack = vm.stack

val sp_before = registers[REGISTER_SP]

in

if sp_before = i2vm 0 then

$raise vm_runtime_error ("Stack underflow.")

else

let

val sp_after = sp_before - i2vm 1

val _ = registers[REGISTER_SP] := sp_after

val i = g1ofg0 (vm2sz sp_after)

(* What follows is a runtime assertion that the upper stack

boundary is not gone past, even though it certainly will

not. This is necessary (assuming one does not use something

such as $UN.prop_assert) because the stack pointer is a

vmint, whose bounds cannot be proven at compile time.

If you comment out the assertloc, the program will not pass

typechecking.

Compilers for many other languages will just insert such

checks willy-nilly, leading programmers to turn off such

instrumentation in the very code they provide to users.

One might be tempted to use Size_t instead for the stack

pointer, but what if the instruction set were later

augmented with ways to read from or write into the stack

pointer? *)

val _ = assertloc (i < vmarray_vt_length stack)

in

stack[i]

end

end

fn {}

push (vm : &vm_vt,

x : vmint) :

void =

let

macdef registers = vm.registers

macdef stack = vm.stack

val sp_before = registers[REGISTER_SP]

val i = g1ofg0 (vm2sz sp_before)

in

if vmarray_vt_length stack <= i then

$raise vm_runtime_error ("Stack overflow.")

else

let

val sp_after = sp_before + i2vm 1

in

registers[REGISTER_SP] := sp_after;

stack[i] := x

end

end

fn {}

fetch_data (vm : &vm_vt,

index : vmint) :

vmint =

let

macdef data = vm.data

val i = g1ofg0 (vm2sz index)

in

if vmarray_vt_length data <= i then

$raise vm_runtime_error ("Fetch from outside the data section.")

else

data[i]

end

fn {}

store_data (vm : &vm_vt,

index : vmint,

x : vmint) :

void =

let

macdef data = vm.data

val i = g1ofg0 (vm2sz index)

in

if vmarray_vt_length data <= i then

$raise vm_runtime_error ("Store to outside the data section.")

else

data[i] := x

end

fn {}

get_argument (vm : &vm_vt) :

vmint =

let

macdef code = vm.code

macdef registers = vm.registers

val pc = registers[REGISTER_PC]

val i = g1ofg0 (vm2sz pc)

in

if vmarray_vt_length code <= i + i2sz 4 then

$raise (vm_runtime_error

("The program counter is out of bounds."))

else

let

(* The data is stored little-endian. *)

val byte0 = byte2vm code[i]

val byte1 = byte2vm code[i + i2sz 1]

val byte2 = byte2vm code[i + i2sz 2]

val byte3 = byte2vm code[i + i2sz 3]

in

(byte0) lor (byte1 << 8) lor (byte2 << 16) lor (byte3 << 24)

end

end

fn {}

skip_argument (vm : &vm_vt) :

void =

let

macdef registers = vm.registers

val pc = registers[REGISTER_PC]

in

registers[REGISTER_PC] := pc + i2vm 4

end

extern fun {}

unary_operation$inner : vmint -<> vmint

fn {}

unary_operation (vm : &vm_vt) :

void =

let

macdef registers = vm.registers

macdef stack = vm.stack

val sp = registers[REGISTER_SP]

val i = g1ofg0 (vm2sz (sp))

prval _ = lemma_g1uint_param i

in

if i = i2sz 0 then

$raise vm_runtime_error ("Stack underflow.")

else

let

val _ = assertloc (i < vmarray_vt_length stack)

(* The actual unary operation is inserted here during

template expansion. *)

val result = unary_operation$inner<> (stack[i - 1])

in

stack[i - 1] := result

end

end

extern fun {}

binary_operation$inner : (vmint, vmint) -<> vmint

fn {}

binary_operation (vm : &vm_vt) :

void =

let

macdef registers = vm.registers

macdef stack = vm.stack

val sp_before = registers[REGISTER_SP]

val i = g1ofg0 (vm2sz (sp_before))

prval _ = lemma_g1uint_param i

in

if i <= i2sz 1 then

$raise vm_runtime_error ("Stack underflow.")

else

let

val _ = registers[REGISTER_SP] := sp_before - i2vm 1

val _ = assertloc (i < vmarray_vt_length stack)

(* The actual binary operation is inserted here during

template expansion. *)

val result =

binary_operation$inner<> (stack[i - 2], stack[i - 1])

in

stack[i - 2] := result

end

end

fn {}

uop_neg (vm : &vm_vt) :

void =

let

implement {}

unary_operation$inner (x) =

twos_complement x

in

unary_operation (vm)

end

fn {}

uop_not (vm : &vm_vt) :

void =

let

implement {}

unary_operation$inner (x) =

logical_not x

in

unary_operation (vm)

end

fn {}

binop_add (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x + y

in

binary_operation (vm)

end

fn {}

binop_sub (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x - y

in

binary_operation (vm)

end

fn {}

binop_mul (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x \signed_mul y

in

binary_operation (vm)

end

fn {}

binop_div (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x \signed_div y

in

binary_operation (vm)

end

fn {}

binop_mod (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x \signed_mod y

in

binary_operation (vm)

end

fn {}

binop_eq (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x \equality y

in

binary_operation (vm)

end

fn {}

binop_ne (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x \inequality y

in

binary_operation (vm)

end

fn {}

binop_lt (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x \signed_lt y

in

binary_operation (vm)

end

fn {}

binop_gt (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x \signed_gt y

in

binary_operation (vm)

end

fn {}

binop_le (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x \signed_lte y

in

binary_operation (vm)

end

fn {}

binop_ge (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x \signed_gte y

in

binary_operation (vm)

end

fn {}

binop_and (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x \logical_and y

in

binary_operation (vm)

end

fn {}

binop_or (vm : &vm_vt) :

void =

let

implement {}

binary_operation$inner (x, y) =

x \logical_or y

in

binary_operation (vm)

end

fn {}

do_push (vm : &vm_vt) :

void =

let

val arg = get_argument (vm)

in

push (vm, arg);

skip_argument (vm)

end

fn {}

do_fetch (vm : &vm_vt) :

void =

let

val i = get_argument (vm)

val x = fetch_data (vm, i)

in

push (vm, x);

skip_argument (vm)

end

fn {}

do_store (vm : &vm_vt) :

void =

let

val i = get_argument (vm)

val x = pop (vm)

in

store_data (vm, i, x);

skip_argument (vm)

end

fn {}

do_jmp (vm : &vm_vt) :

void =

let

macdef registers = vm.registers

val arg = get_argument (vm)

val pc = registers[REGISTER_PC]

in

registers[REGISTER_PC] := pc + arg

end

fn {}

do_jz (vm : &vm_vt) :

void =

let

val x = pop (vm)

in

if x = i2vm 0 then

do_jmp (vm)

else

skip_argument (vm)

end

fn {}

do_prtc (f_output : FILEref,

vm : &vm_vt) :

void =

let

val x = pop (vm)

in

fileref_putc (f_output, vm2i x)

end

fn {}

do_prti (f_output : FILEref,

vm : &vm_vt) :

void =

let

val x = pop (vm)

in

fprint! (f_output, vm2i x)

end

fn {}

do_prts (f_output : FILEref,

vm : &vm_vt) :

void =

let

val i = g1ofg0 (vm2sz (pop (vm)))

in

if vmstrings_section_vt_length (vm.strings) <= i then

$raise vm_runtime_error ("String index out of bounds.")

else

vmstring_fprint (f_output, vm.strings, i)

end

fn

vm_step (f_output : FILEref,

vm : &vm_vt,

machine_halt : &bool,

bad_opcode : &bool) :

void =

let

macdef code = vm.code

macdef registers = vm.registers

val pc = registers[REGISTER_PC]

val i = g1ofg0 (vm2sz (pc))

prval _ = lemma_g1uint_param i

in

if vmarray_vt_length (code) <= i then

$raise (vm_runtime_error

("The program counter is out of bounds."))

else

let

val _ = registers[REGISTER_PC] := pc + i2vm 1

val opcode = code[i]

val u_opcode = byte2uint0 opcode

in

(* Dispatch by bifurcation on the bit pattern of the

opcode. This method is logarithmic in the number

of opcode values. *)

machine_halt := false;

bad_opcode := false;

if (u_opcode land (~0x1FU)) = 0U then

begin

if (u_opcode land 0x10U) = 0U then

begin

if (u_opcode land 0x08U) = 0U then

begin

if (u_opcode land 0x04U) = 0U then

begin

if (u_opcode land 0x02U) = 0U then

begin

if (u_opcode land 0x01U) = 0U then

(* OP_HALT *)

machine_halt := true

else

binop_add (vm)