Compiler/virtual machine interpreter: Difference between revisions

Content added Content deleted
Line 1,342: Line 1,342:
(* *)
(* *)


datavtype instruction_vt =
datatype instruction_t =
| instruction_t_1 of (byte)
| instruction_vt_1 of (byte)
| instruction_t_5 of (byte, byte, byte, byte, byte)
| instruction_vt_5 of (byte, byte, byte, byte, byte)


#define OPCODE_COUNT 24
#define OPCODE_COUNT 24
Line 1,478: Line 1,478:
(arr : &(@[String0][OPCODE_COUNT]),
(arr : &(@[String0][OPCODE_COUNT]),
line : string n) :
line : string n) :
instruction_t =
instruction_vt =
let
let
val bad_instruction = "Bad VM instruction."
val bad_instruction = "Bad VM instruction."
Line 1,495: Line 1,495:
fn
fn
finish_push () :
finish_push () :
instruction_t =
instruction_vt =
let
let
val i1 = skip_whitespace (line, n, start_of_argument)
val i1 = skip_whitespace (line, n, start_of_argument)
Line 1,502: Line 1,502:
in
in
(* Little-endian storage. *)
(* Little-endian storage. *)
instruction_t_5 (opcode, vmint_byte0 arg, vmint_byte1 arg,
instruction_vt_5 (opcode, vmint_byte0 arg, vmint_byte1 arg,
vmint_byte2 arg, vmint_byte3 arg)
vmint_byte2 arg, vmint_byte3 arg)
end
end
Line 1,508: Line 1,508:
fn
fn
finish_fetch_or_store () :
finish_fetch_or_store () :
instruction_t =
instruction_vt =
let
let
val i1 = skip_whitespace (line, n, start_of_argument)
val i1 = skip_whitespace (line, n, start_of_argument)
Line 1,522: Line 1,522:
in
in
(* Little-endian storage. *)
(* Little-endian storage. *)
instruction_t_5 (opcode, vmint_byte0 arg, vmint_byte1 arg,
instruction_vt_5 (opcode, vmint_byte0 arg, vmint_byte1 arg,
vmint_byte2 arg, vmint_byte3 arg)
vmint_byte2 arg, vmint_byte3 arg)
end
end
Line 1,529: Line 1,529:
fn
fn
finish_jmp_or_jz () :
finish_jmp_or_jz () :
instruction_t =
instruction_vt =
let
let
val i1 = skip_whitespace (line, n, start_of_argument)
val i1 = skip_whitespace (line, n, start_of_argument)
Line 1,543: Line 1,543:
in
in
(* Little-endian storage. *)
(* Little-endian storage. *)
instruction_t_5 (opcode, vmint_byte0 arg, vmint_byte1 arg,
instruction_vt_5 (opcode, vmint_byte0 arg, vmint_byte1 arg,
vmint_byte2 arg, vmint_byte3 arg)
vmint_byte2 arg, vmint_byte3 arg)
end
end
Line 1,554: Line 1,554:
| OP_JMP => finish_jmp_or_jz ()
| OP_JMP => finish_jmp_or_jz ()
| OP_JZ => finish_jmp_or_jz ()
| OP_JZ => finish_jmp_or_jz ()
| _ => instruction_t_1 (opcode)
| _ => instruction_vt_1 (opcode)
end
end


Line 1,560: Line 1,560:
read_instructions (f : FILEref,
read_instructions (f : FILEref,
arr : &(@[String0][OPCODE_COUNT])) :
arr : &(@[String0][OPCODE_COUNT])) :
(List_vt (instruction_t), Size_t) =
(List_vt (instruction_vt), Size_t) =
(* Read the instructions from the input, producing a list of
(* Read the instructions from the input, producing a list of
instruction_t objects, and also calculating the total
instruction_vt objects, and also calculating the total
number of bytes in the instructions. *)
number of bytes in the instructions. *)
let
let
fun
fun
loop (arr : &(@[String0][OPCODE_COUNT]),
loop (arr : &(@[String0][OPCODE_COUNT]),
lst : List_vt (instruction_t),
lst : List_vt (instruction_vt),
bytes_needed : Size_t) :
bytes_needed : Size_t) :
@(List_vt (instruction_t), Size_t) =
@(List_vt (instruction_vt), Size_t) =
if fileref_is_eof f then
if fileref_is_eof f then
@(list_vt_reverse lst, bytes_needed)
@(list_vt_reverse lst, bytes_needed)
Line 1,589: Line 1,589:
in
in
case+ instruction of
case+ instruction of
| instruction_t_1 _ =>
| instruction_vt_1 _ =>
loop (arr, instruction :: lst, bytes_needed + i2sz 1)
loop (arr, instruction :: lst, bytes_needed + i2sz 1)
| instruction_t_5 _ =>
| instruction_vt_5 _ =>
loop (arr, instruction :: lst, bytes_needed + i2sz 5)
loop (arr, instruction :: lst, bytes_needed + i2sz 5)
end
end
Line 1,601: Line 1,601:
fn
fn
list_of_instructions_to_code {bytes_needed : int}
list_of_instructions_to_code {bytes_needed : int}
(lst : List_vt (instruction_t),
(lst : List_vt (instruction_vt),
bytes_needed : size_t bytes_needed) :
bytes_needed : size_t bytes_needed) :
[bytes_needed : int]
[bytes_needed : int]
Line 1,610: Line 1,610:
loop {n : int | 0 <= n} .<n>.
loop {n : int | 0 <= n} .<n>.
(code : &vmarray_vt (byte, bytes_needed),
(code : &vmarray_vt (byte, bytes_needed),
lst : list_vt (instruction_t, n),
lst : list_vt (instruction_vt, n),
i : Size_t) : void =
i : Size_t) : void =
case+ lst of
case+ lst of
| ~ NIL => ()
| ~ NIL => ()
| ~ (instruction_t_1 (byte1) :: tail) =>
| ~ head :: tail =>
let
begin
val _ = assertloc (i < bytes_needed)
case head of
| ~ instruction_vt_1 (byte1) =>
in
code[i] := byte1;
let
loop (code, tail, i + i2sz 1)
val _ = assertloc (i < bytes_needed)
end
in
code[i] := byte1;
| ~ (instruction_t_5 (byte1, byte2, byte3, byte4, byte5)
:: tail) =>
loop (code, tail, i + i2sz 1)
let
end
val _ = assertloc (i + i2sz 4 < bytes_needed)
| ~ instruction_vt_5 (byte1, byte2, byte3, byte4, byte5) =>
in
let
val _ = assertloc (i + i2sz 4 < bytes_needed)
code[i] := byte1;
code[i + i2sz 1] := byte2;
in
code[i + i2sz 2] := byte3;
code[i] := byte1;
code[i + i2sz 3] := byte4;
code[i + i2sz 1] := byte2;
code[i + i2sz 4] := byte5;
code[i + i2sz 2] := byte3;
loop (code, tail, i + i2sz 5)
code[i + i2sz 3] := byte4;
code[i + i2sz 4] := byte5;
loop (code, tail, i + i2sz 5)
end
end
end