1804 lines
47 KiB
Plaintext
1804 lines
47 KiB
Plaintext
(*
|
||
Usage: vm [INPUTFILE [OUTPUTFILE]]
|
||
If INPUTFILE or OUTPUTFILE is "-" or missing, then standard input
|
||
or standard output is used, respectively.
|
||
|
||
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 (hopefully) 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);
|
||
}
|
||
|
||
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. *)
|
||
(* *)
|
||
|
||
datavtype instruction_vt =
|
||
| instruction_vt_1 of (byte)
|
||
| instruction_vt_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_vt =
|
||
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_vt =
|
||
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_vt_5 (opcode, vmint_byte0 arg, vmint_byte1 arg,
|
||
vmint_byte2 arg, vmint_byte3 arg)
|
||
end
|
||
|
||
fn
|
||
finish_fetch_or_store () :
|
||
instruction_vt =
|
||
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_vt_5 (opcode, vmint_byte0 arg, vmint_byte1 arg,
|
||
vmint_byte2 arg, vmint_byte3 arg)
|
||
end
|
||
end
|
||
|
||
fn
|
||
finish_jmp_or_jz () :
|
||
instruction_vt =
|
||
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_vt_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_vt_1 (opcode)
|
||
end
|
||
|
||
fn
|
||
read_instructions (f : FILEref,
|
||
arr : &(@[String0][OPCODE_COUNT])) :
|
||
(List_vt (instruction_vt), Size_t) =
|
||
(* Read the instructions from the input, producing a list of
|
||
instruction_vt objects, and also calculating the total
|
||
number of bytes in the instructions. *)
|
||
let
|
||
fun
|
||
loop (arr : &(@[String0][OPCODE_COUNT]),
|
||
lst : List_vt (instruction_vt),
|
||
bytes_needed : Size_t) :
|
||
@(List_vt (instruction_vt), 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_vt_1 _ =>
|
||
loop (arr, instruction :: lst, bytes_needed + i2sz 1)
|
||
| instruction_vt_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_vt),
|
||
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_vt, n),
|
||
i : Size_t) : void =
|
||
case+ lst of
|
||
| ~ NIL => ()
|
||
| ~ head :: tail =>
|
||
begin
|
||
case head of
|
||
| ~ instruction_vt_1 (byte1) =>
|
||
let
|
||
val _ = assertloc (i < bytes_needed)
|
||
in
|
||
code[i] := byte1;
|
||
loop (code, tail, i + i2sz 1)
|
||
end
|
||
| ~ instruction_vt_5 (byte1, byte2, byte3, byte4, byte5) =>
|
||
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
|
||
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)
|
||
end
|
||
else
|
||
begin
|
||
if (u_opcode land 0x01U) = 0U then
|
||
binop_sub (vm)
|
||
else
|
||
binop_mul (vm)
|
||
end
|
||
end
|
||
else
|
||
begin
|
||
if (u_opcode land 0x02U) = 0U then
|
||
begin
|
||
if (u_opcode land 0x01U) = 0U then
|
||
binop_div (vm)
|
||
else
|
||
binop_mod (vm)
|
||
end
|
||
else
|
||
begin
|
||
if (u_opcode land 0x01U) = 0U then
|
||
binop_lt (vm)
|
||
else
|
||
binop_gt (vm)
|
||
end
|
||
end
|
||
end
|
||
else
|
||
begin
|
||
if (u_opcode land 0x04U) = 0U then
|
||
begin
|
||
if (u_opcode land 0x02U) = 0U then
|
||
begin
|
||
if (u_opcode land 0x01U) = 0U then
|
||
binop_le (vm)
|
||
else
|
||
binop_ge (vm)
|
||
end
|
||
else
|
||
begin
|
||
if (u_opcode land 0x01U) = 0U then
|
||
binop_eq (vm)
|
||
else
|
||
binop_ne (vm)
|
||
end
|
||
end
|
||
else
|
||
begin
|
||
if (u_opcode land 0x02U) = 0U then
|
||
begin
|
||
if (u_opcode land 0x01U) = 0U then
|
||
binop_and (vm)
|
||
else
|
||
binop_or (vm)
|
||
end
|
||
else
|
||
begin
|
||
if (u_opcode land 0x01U) = 0U then
|
||
uop_neg (vm)
|
||
else
|
||
uop_not (vm)
|
||
end
|
||
end
|
||
end
|
||
end
|
||
else
|
||
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
|
||
do_prtc (f_output, vm)
|
||
else
|
||
do_prti (f_output, vm)
|
||
end
|
||
else
|
||
begin
|
||
if (u_opcode land 0x01U) = 0U then
|
||
do_prts (f_output, vm)
|
||
else
|
||
do_fetch (vm)
|
||
end
|
||
end
|
||
else
|
||
begin
|
||
if (u_opcode land 0x02U) = 0U then
|
||
begin
|
||
if (u_opcode land 0x01U) = 0U then
|
||
do_store (vm)
|
||
else
|
||
do_push (vm)
|
||
end
|
||
else
|
||
begin
|
||
if (u_opcode land 0x01U) = 0U then
|
||
do_jmp (vm)
|
||
else
|
||
do_jz (vm)
|
||
end
|
||
end
|
||
end
|
||
else
|
||
bad_opcode := true
|
||
end
|
||
end
|
||
else
|
||
bad_opcode := true
|
||
end
|
||
end
|
||
|
||
fn
|
||
vm_continue (f_output : FILEref,
|
||
vm : &vm_vt) :
|
||
void =
|
||
let
|
||
fun
|
||
loop (vm : &vm_vt,
|
||
machine_halt : &bool,
|
||
bad_opcode : &bool) : void =
|
||
if ~machine_halt && ~bad_opcode then
|
||
begin
|
||
vm_step (f_output, vm, machine_halt, bad_opcode);
|
||
loop (vm, machine_halt, bad_opcode)
|
||
end
|
||
|
||
var machine_halt : bool = false
|
||
var bad_opcode : bool = false
|
||
in
|
||
loop (vm, machine_halt, bad_opcode);
|
||
if bad_opcode then
|
||
$raise vm_runtime_error ("Unrecognized opcode at runtime.")
|
||
end
|
||
|
||
fn
|
||
vm_initialize (vm : &vm_vt) :
|
||
void =
|
||
let
|
||
macdef data = vm.data
|
||
macdef registers = vm.registers
|
||
in
|
||
vmarray_vt_fill (data, i2vm 0);
|
||
registers[REGISTER_PC] := i2vm 0;
|
||
registers[REGISTER_SP] := i2vm 0
|
||
end
|
||
|
||
|
||
fn
|
||
vm_run (f_output : FILEref,
|
||
vm : &vm_vt) :
|
||
void =
|
||
begin
|
||
vm_initialize (vm);
|
||
vm_continue (f_output, vm)
|
||
end
|
||
|
||
(********************************************************************)
|
||
|
||
implement
|
||
main0 (argc, argv) =
|
||
{
|
||
val inpfname =
|
||
if 2 <= argc then
|
||
$UN.cast{string} argv[1]
|
||
else
|
||
"-"
|
||
val outfname =
|
||
if 3 <= argc then
|
||
$UN.cast{string} argv[2]
|
||
else
|
||
"-"
|
||
|
||
val inpf =
|
||
if (inpfname : string) = "-" then
|
||
stdin_ref
|
||
else
|
||
fileref_open_exn (inpfname, file_mode_r)
|
||
|
||
val outf =
|
||
if (outfname : string) = "-" then
|
||
stdout_ref
|
||
else
|
||
fileref_open_exn (outfname, file_mode_w)
|
||
|
||
(* The following order must match that established by
|
||
OP_HALT, OP_ADD, OP_SUB, etc. *)
|
||
var opcode_order =
|
||
@[String0][OPCODE_COUNT] ("halt", // 00000 bit pattern
|
||
"add", // 00001
|
||
"sub", // 00010
|
||
"mul", // 00011
|
||
"div", // 00100
|
||
"mod", // 00101
|
||
"lt", // 00110
|
||
"gt", // 00111
|
||
"le", // 01000
|
||
"ge", // 01001
|
||
"eq", // 01010
|
||
"ne", // 01011
|
||
"and", // 01100
|
||
"or", // 01101
|
||
"neg", // 01110
|
||
"not", // 01111
|
||
"prtc", // 10000
|
||
"prti", // 10001
|
||
"prts", // 10010
|
||
"fetch", // 10011
|
||
"store", // 10100
|
||
"push", // 10101
|
||
"jmp", // 10110
|
||
"jz") // 10111
|
||
|
||
val _ = ensure_that_vmint_is_suitable ()
|
||
var vm = read_vm (inpf, opcode_order)
|
||
val _ = vm_run (outf, vm)
|
||
val _ = vm_vt_free vm
|
||
}
|
||
|
||
(********************************************************************)
|