1804 lines
47 KiB
Text
1804 lines
47 KiB
Text
|
(*
|
|||
|
|
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
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
(********************************************************************)
|