proof/FINDINGS.md's Isabelle/HOL word-source sweep (§4) flagged five real defects; this fixes all five and records resolution in that doc: - EXECUTE (system_words.c): cast a popped cell straight to a DictEntry* and called through it with only a null check. Now validates via a new shared vm_dict_entry_ok(), promoted out of starforth_words.c's ENTROPY@/ENTROPY! guard (dictionary_management.c) so EXECUTE gets the same live-entry check. - ? and DUMP (format_words.c): dereferenced the popped cell as a raw host pointer, bypassing vm_addr_ok entirely (out-of-VM-bounds read). Both now go through VM_ADDR/vm_addr_ok/vm_load_cell/vm_ptr like every other memory word (@, `,`, editor_words.c). - TYPE (io_words.c): bounds check computed addr+count in signed 64-bit arithmetic, which can overflow and bypass the check on large operands. Replaced with vm_addr_ok(), which is written to avoid that overflow. - DECIMAL/HEX/OCTAL (format_words.c): wrote only the BASE memory cell, never vm->base, the host-mirror field number-output words actually read via current_base() -- so these words silently affected number parsing but never printing. Now call the existing vm_set_base() (previously only used at boot init), which updates both. vm_get_base/vm_set_base promoted to public declarations in include/vm.h. - ALIGN vs ALLOT/,/C,/2, (dictionary_words.c): disagreed on dictionary growth ceiling (2MB vs 5MB). Investigated which was correct rather than blindly widening: vm_get_block_addr() maps block N to vm->memory + N*BLOCK_SIZE across the full 5MB arena, and USER_BLOCKS_START (block 2048) lines up exactly with DICTIONARY_MEMORY_SIZE -- so ALLOT/,/C,/2, letting `here` grow past 2MB could silently corrupt live block/user data sharing that memory. Tightened ALLOT/,/C,/2, to DICTIONARY_MEMORY_SIZE to match ALIGN. Verified: hosted (amd64) and kernel (amd64, __STARKERNEL__) both build clean with -Wall -Werror; hosted POST suite 1012/1012 passing (0 regressions); manually exercised EXECUTE, ?/DUMP, TYPE, HEX/DECIMAL/OCTAL, and large-ALLOT rejection in the REPL. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014Qf6YcnHgaEtEygq3knx19
263 lines
8.0 KiB
C
263 lines
8.0 KiB
C
/*
|
||
StarForth — Steady-State Virtual Machine Runtime
|
||
|
||
Copyright (c) 2023–2025 Robert A. James
|
||
All rights reserved.
|
||
|
||
This file is part of the StarForth project.
|
||
|
||
Licensed under the StarForth License, Version 1.0 (the "License");
|
||
you may not use this file except in compliance with the License.
|
||
|
||
You may obtain a copy of the License at:
|
||
https://github.com/star.4th@proton.me/StarForth/LICENSE.txt
|
||
|
||
This software is provided "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||
express or implied, including but not limited to the warranties of
|
||
merchantability, fitness for a particular purpose, and noninfringement.
|
||
|
||
See the License for the specific language governing permissions and
|
||
limitations under the License.
|
||
|
||
StarForth — Steady-State Virtual Machine Runtime
|
||
Copyright (c) 2023–2025 Robert A. James
|
||
All rights reserved.
|
||
|
||
This file is part of the StarForth project.
|
||
|
||
Licensed under the StarForth License, Version 1.0 (the "License");
|
||
you may not use this file except in compliance with the License.
|
||
|
||
You may obtain a copy of the License at:
|
||
https://github.com/star.4th@proton.me/StarForth/LICENSE.txt
|
||
|
||
This software is provided "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||
express or implied, including but not limited to the warranties of
|
||
merchantability, fitness for a particular purpose, and noninfringement.
|
||
|
||
See the License for the specific language governing permissions and
|
||
limitations under the License.
|
||
|
||
*/
|
||
|
||
/* io_words.c - FORTH-79 I/O & Terminal Words */
|
||
#include "include/io_words.h"
|
||
#include "../../include/word_registry.h"
|
||
#include "../../include/log.h"
|
||
#include "../../include/platform_io.h"
|
||
#include <stdio.h>
|
||
|
||
|
||
/**
|
||
* @brief FORTH word EMIT - Output character to terminal
|
||
* @param vm Pointer to the VM structure
|
||
* @details Stack effect: ( c -- )
|
||
* Outputs the character from top of stack to the terminal
|
||
*/
|
||
static void io_word_emit(VM *vm) {
|
||
if (vm->dsp < 0) {
|
||
vm->error = 1;
|
||
return;
|
||
}
|
||
|
||
char c = (char) vm->data_stack[vm->dsp--];
|
||
putchar(c);
|
||
fflush(stdout);
|
||
}
|
||
|
||
/**
|
||
* @brief FORTH word CR - Output carriage return
|
||
* @param vm Pointer to the VM structure
|
||
* @details Stack effect: ( -- )
|
||
* Outputs a newline character to the terminal
|
||
*/
|
||
static void io_word_cr(VM *vm) {
|
||
(void)vm;
|
||
putchar('\n');
|
||
fflush(stdout);
|
||
}
|
||
|
||
/**
|
||
* @brief FORTH word KEY - Input character from terminal
|
||
* @param vm Pointer to the VM structure
|
||
* @details Stack effect: ( -- c )
|
||
* Reads one character from terminal and pushes it to stack
|
||
*/
|
||
static void io_word_key(VM *vm) {
|
||
if (vm->dsp >= STACK_SIZE - 1) {
|
||
vm->error = 1;
|
||
return;
|
||
}
|
||
|
||
int c = getchar();
|
||
vm->data_stack[++vm->dsp] = (cell_t) c;
|
||
}
|
||
|
||
/**
|
||
* @brief FORTH word ?TERMINAL - Check if input is available
|
||
* @param vm Pointer to the VM structure
|
||
* @details Stack effect: ( -- flag )
|
||
* Pushes true if input is available, false otherwise
|
||
*/
|
||
static void io_word_question_terminal(VM *vm) {
|
||
if (vm->dsp >= STACK_SIZE - 1) {
|
||
vm->error = 1;
|
||
return;
|
||
}
|
||
|
||
vm->data_stack[++vm->dsp] = sf_terminal_ready() ? -1 : 0;
|
||
}
|
||
|
||
/**
|
||
* @brief FORTH word TYPE - Output string of characters
|
||
* @param vm Pointer to the VM structure
|
||
* @details Stack effect: ( addr u -- )
|
||
* Outputs u characters from memory starting at addr
|
||
*/
|
||
static void io_word_type(VM *vm) {
|
||
if (vm->dsp < 1) {
|
||
log_message(LOG_ERROR, "TYPE: Data stack underflow");
|
||
vm->error = 1;
|
||
return;
|
||
}
|
||
|
||
cell_t count = vm_pop(vm);
|
||
vaddr_t addr = VM_ADDR(vm_pop(vm));
|
||
|
||
// Bounds check via vm_addr_ok (avoids the addr+count overflow a manual
|
||
// sum would risk for large signed operands)
|
||
if (count < 0 || !vm_addr_ok(vm, addr, (size_t) count)) {
|
||
log_message(LOG_ERROR, "TYPE: Invalid range [addr=%llu, count=%ld)",
|
||
(unsigned long long) addr, (long) count);
|
||
vm->error = 1;
|
||
return;
|
||
}
|
||
|
||
// Output characters from VM memory
|
||
const uint8_t *src = vm_ptr(vm, addr);
|
||
for (cell_t i = 0; i < count; i++) {
|
||
putchar(src[i]);
|
||
}
|
||
fflush(stdout);
|
||
|
||
log_message(LOG_DEBUG, "TYPE: Output %ld characters from address %llu",
|
||
(long) count, (unsigned long long) addr);
|
||
}
|
||
|
||
/**
|
||
* @brief FORTH word SPACE - Output one space character
|
||
* @param vm Pointer to the VM structure
|
||
* @details Stack effect: ( -- )
|
||
* Outputs a single space character to terminal
|
||
*/
|
||
static void io_word_space(VM *vm) {
|
||
(void)vm;
|
||
putchar(' ');
|
||
fflush(stdout);
|
||
}
|
||
|
||
/**
|
||
* @brief FORTH word SPACES - Output multiple spaces
|
||
* @param vm Pointer to the VM structure
|
||
* @details Stack effect: ( n -- )
|
||
* Outputs n space characters to terminal
|
||
*/
|
||
static void io_word_spaces(VM *vm) {
|
||
if (vm->dsp < 0) {
|
||
vm->error = 1;
|
||
return;
|
||
}
|
||
|
||
cell_t count = vm->data_stack[vm->dsp--];
|
||
|
||
if (count < 0) return;
|
||
|
||
for (cell_t i = 0; i < count; i++) {
|
||
putchar(' ');
|
||
}
|
||
fflush(stdout);
|
||
}
|
||
|
||
/* (do-string) — runtime called by compiled ." ; reads inline string from
|
||
* threaded code via the return-stack IP, prints it, then advances IP past
|
||
* the padded inline block. NOT immediate.
|
||
*
|
||
* Inline layout immediately after the (do-string) cell in the thread:
|
||
* [1 length byte][n string bytes][padding to next cell boundary]
|
||
*/
|
||
static void io_runtime_do_string(VM *vm) {
|
||
if (vm->rsp < 0) { vm->error = 1; return; }
|
||
/* return_stack[rsp] holds ip+1 as a raw C pointer — points at inline data */
|
||
uint8_t *data = (uint8_t *)(uintptr_t)vm->return_stack[vm->rsp];
|
||
if (!data) { vm->error = 1; return; }
|
||
uint8_t n = data[0];
|
||
for (uint8_t i = 0; i < n; i++)
|
||
putchar((unsigned char)data[1 + i]);
|
||
fflush(stdout);
|
||
/* advance IP past inline block (length byte + string bytes, cell-aligned) */
|
||
size_t skip = 1 + (size_t)n;
|
||
size_t padded = (skip + (sizeof(cell_t) - 1)) & ~(sizeof(cell_t) - 1);
|
||
vm->return_stack[vm->rsp] = (cell_t)(uintptr_t)(data + padded);
|
||
}
|
||
|
||
/* ." ( "ccc<quote>" -- )
|
||
* Immediate. Interpretation: parse and print the string directly.
|
||
* Compilation: compile (do-string) + inline [len][chars][pad].
|
||
*/
|
||
static void io_word_dot_quote(VM *vm) {
|
||
const char *src = vm->input_buffer;
|
||
size_t pos = vm->input_pos;
|
||
size_t end = vm->input_length;
|
||
|
||
if (!src || pos > end) {
|
||
vm->error = 1;
|
||
return;
|
||
}
|
||
if (pos < end && src[pos] == ' ') pos++;
|
||
|
||
size_t start = pos;
|
||
while (pos < end && src[pos] != '"') pos++;
|
||
if (pos >= end) { vm->error = 1; return; }
|
||
|
||
size_t n = pos - start;
|
||
if (n > 255) n = 255; /* single length byte — clamp silently */
|
||
vm->input_pos = pos + 1;
|
||
|
||
if (vm->mode == MODE_INTERPRET) {
|
||
for (size_t i = 0; i < n; i++)
|
||
putchar((unsigned char)src[start + i]);
|
||
fflush(stdout);
|
||
return;
|
||
}
|
||
|
||
/* Compilation: emit (do-string) cell then inline [len][chars][pad] */
|
||
DictEntry *do_str = vm_find_word(vm, "(do-string)", 11);
|
||
if (!do_str) { vm->error = 1; return; }
|
||
vm_compile_word(vm, do_str);
|
||
|
||
size_t skip = 1 + n;
|
||
size_t padded = (skip + (sizeof(cell_t) - 1)) & ~(sizeof(cell_t) - 1);
|
||
uint8_t *raw = (uint8_t *)vm_allot(vm, padded);
|
||
if (!raw) { vm->error = 1; return; }
|
||
raw[0] = (uint8_t)n;
|
||
for (size_t i = 0; i < n; i++) raw[1 + i] = (uint8_t)src[start + i];
|
||
for (size_t i = 1 + n; i < padded; i++) raw[i] = 0;
|
||
}
|
||
|
||
/*
|
||
* @brief Register all I/O words with the VM
|
||
* @param vm Pointer to the VM structure
|
||
* @details Registers all FORTH-79 I/O and terminal words with the virtual machine
|
||
*/
|
||
void register_io_words(VM *vm) {
|
||
register_word(vm, "EMIT", io_word_emit);
|
||
register_word(vm, "CR", io_word_cr);
|
||
register_word(vm, "KEY", io_word_key);
|
||
register_word(vm, "?TERMINAL", io_word_question_terminal);
|
||
register_word(vm, "TYPE", io_word_type);
|
||
register_word(vm, "SPACE", io_word_space);
|
||
register_word(vm, "SPACES", io_word_spaces);
|
||
register_word(vm, "(do-string)", io_runtime_do_string);
|
||
register_word(vm, ".\"", io_word_dot_quote);
|
||
vm_make_immediate(vm);
|
||
} |