Oska runtime

oskac run <file.osk> [--format=json] [-- args...] checks one file and, if the check reports no diagnostic, runs it in the interpreter (oska-run). oskac test <file.osk> [--format=json] [--integration] runs its test blocks instead (see Tests). The interpreter executes the checker's checked program (ADR 0007); the rules it follows are in the "Runtime" section of design.md. This page describes how a run ends and the codes the runtime reports. Checker codes are in checker.md.

Exit codes

Exit codeMeaning
0main returned Ok or ().
1The checker refused the program, or main returned Err: an expected failure.
2The program uses something the interpreter cannot run yet (E0370, E0371, E0380). Nothing ran.
101The program panicked: it has a bug.

Refusals

Before a program starts, the runtime checks that it can run all of it, reached or not, so a program never fails halfway through because of a gap in the interpreter. A refusal is printed like a checker diagnostic: to stderr, as one JSON object per line with --format=json.

CodeRefusal
E0370main declares a capability that has no runtime yet: Net, NetConnect, NetListen, Spawn, or Sched. Spans main's body. (A main that declares a directory or file capability is already refused by the checker, E0217.)
E0371The program imports a std module that has no runtime yet: std.proc or std.sql, used or not. Spans the module path of the use.
E0380The program uses something the interpreter cannot run yet: a construct the checked program cannot express, a call of a prelude function with no runtime implementation, or a parameter of main that is neither a capability nor Args. The message names the construct, as in the interpreter cannot run a `From`-bound conversion yet; others are a constructor used as a function value, a call of a generic trait's method, and a ? or return in a contract outside any closure (the checker rejects that first, with E0282, so this is a second line of defence). Spans the construct or call, or main's body for a parameter.

Refusal examples

Each refusal has a program that is refused with exactly that code and the same program fixed. The examples run on the in-memory host, so they depend on nothing outside the program.

E0370

fn main(net: Net) -> Result<(), IoError> {
    Ok(())
}

fn main(io: Stdout) -> Result<(), IoError> {
    io.println("hello")
}

E0371

use std.sql

fn main() {}

use std.html

fn main() {}

E0380

fn main() {
    let make = Some
    let x: Option<Int> = make(1)
}

fn main() {
    let x: Option<Int> = Some(1)
}

Panics

A panic stops the program where a bug happened. It has a stable P-code, a message, and the span of the expression that panicked. Without --format=json, it is printed to stderr like a diagnostic, file.osk: error[P0004]: division by zero: ... (bytes 61..67). With --format=json, it is printed to stderr as one diagnostic object, in the same shape as the checker's (see ast.md):

{"code":"P0004","message":"division by zero: `10 / 0`","span":{"start":61,"end":70}}

Output written before the panic stays written.

Integers of every type, Int and the sized I8 to U64, are checked: arithmetic never wraps.

CodePanic
P0001Integer overflow: the result of +, -, *, /, or unary - does not fit its type, as with a U8 0 - 1 or an I8 -128 / -1. Spans the operation.
P0002Index out of bounds: List.at was given an index below 0 or not below the list's length. Spans the call.
P0003todo() reached. Spans the call.
P0004Division by zero: the right operand of / or % is zero. Spans the operation.
P0005spawn on a finished scope: the handle's scope block has ended, and work never runs outside a scope. Spans the call. This is a second line of defence behind the checker (E0292), which already stops a handle from outliving its block: no checked program can reach this code, so it has no example.
P0006Precondition violated: a requires clause of the function called is false, so the caller broke the contract. The message names the function and quotes the clause's condition. Spans the call. Every call evaluates the function's requires clauses, in every build, in the order written: after the arguments are evaluated and before the body runs. A clause sees the parameters and self. A panic while a clause is evaluated, such as an overflow, is reported as it is, not as P0006.
P0007Postcondition violated: an ensures clause of the function that returned is false, so the function broke its promise. The message names the function, quotes the clause's condition, and names the line and column of the return that broke it, counting columns in characters from 1. Spans the ensures clause. Every return evaluates the function's ensures clauses, in every build, in the order written, with r bound to the value being returned. That covers falling off the end of the body (the return is its last expression, or its closing brace), an early return, and an early exit through ?, where r is the Err or None being returned. A clause sees the parameters and self; a method that changes var self shows its clauses the receiver it ends with. A contract that calls a function with contracts checks those too, and a panic while a clause is evaluated, such as an overflow, is reported as it is, not as P0007.
P0010t.assert(cond) was given false. Fails the test (see Tests). Spans the call.
P0011t.assert_eq(actual, expected) was given two values that differ through Eq. The message shows both, as dbg would. Spans the call.
P0012t.assert_ne(actual, other) was given two equal values. Spans the call.
P0013t.fail(message) was called. The message is message. Spans the call.
P0020Env.secret asked for a variable the environment does not set. Its signature has no room for a missing secret, and running on with a stand-in such as an empty one could let an empty password through. Spans the call.
P0021Calls nest too deep: runaway recursion. The interpreter runs on a thread of its own with a 256 MiB stack, and a call panics instead of starting when calls already nest 50,000 deep, or when so little of that stack is left that the next call could overflow it. The process never crashes on deep recursion: oskac run exits with 101, and under oskac test only the test that recursed fails. Spans the call that would have gone too deep.
P0035String.slice was given indices out of bounds: a start or end below 0 or past the text's length in characters, or a start past the end. Spans the call. Indices count characters (Unicode code points), not bytes.
P0036String.repeat was given a negative count. Spans the call.
P0037String.repeat would build a text over 256 MiB, so the interpreter panics instead of running out of memory. Spans the call.

Panic examples

Each panic has a program that stops with exactly that code and the same program fixed. The P001x examples are tests, because only a test block can fail an assertion, and run under oskac test. P0005 has no example: the checker (E0292) stops a program from keeping a scope handle past its block, so no checked program can reach it.

P0001

fn main() {
    let x: U8 = 255
    let y = x + 1
}

fn main() {
    let x: Int = 255
    let y = x + 1
}

P0002

fn main() {
    let xs: List<Int> = List.new()
    let first = xs.at(0)
}

fn main() {
    let xs: List<Int> = List.new()
    let first = xs.get(0)
}

P0003

fn main() {
    todo()
}

fn main() {}

P0004

fn main() {
    let zero = 0
    let n = 10 / zero
}

fn main() {
    let two = 2
    let n = 10 / two
}

P0006

fn double(x: Int) -> Int
    requires x > 0
{
    x * 2
}

fn main() {
    let y = double(-1)
}

fn double(x: Int) -> Int
    requires x > 0
{
    x * 2
}

fn main() {
    let y = double(1)
}

P0007

fn absolute(x: Int) -> Int
    ensures |r| r >= 0
{
    x
}

fn main() {
    let y = absolute(-1)
}

fn absolute(x: Int) -> Int
    ensures |r| r >= 0
{
    if x < 0 {
        0 - x
    } else {
        x
    }
}

fn main() {
    let y = absolute(-1)
}

P0010

test "is positive" {
    t.assert(1 < 0)
}

test "is positive" {
    t.assert(0 < 1)
}

P0011

test "adds" {
    t.assert_eq(1 + 1, 3)
}

test "adds" {
    t.assert_eq(1 + 1, 2)
}

P0012

test "differs" {
    t.assert_ne(2, 2)
}

test "differs" {
    t.assert_ne(2, 3)
}

P0013

test "not written yet" {
    t.fail("write this test")
}

test "written" {
    t.assert(true)
}

P0020

fn main(env: Env) {
    let key = env.secret("API_KEY")
}

fn main(env: Env) {
    let key = env.get("API_KEY")
}

P0021

fn down(n: Int) -> Int {
    1 + down(n - 1)
}

fn main() {
    let depth = down(10)
}

fn down(n: Int) -> Int {
    if n == 0 { 0 } else { 1 + down(n - 1) }
}

fn main() {
    let depth = down(10)
}

P0035

fn main() {
    let part = "abc".slice(0, 10)
}

fn main() {
    let part = "abc".slice(0, 2)
}

P0036

fn main() {
    let line = "ab".repeat(-1)
}

fn main() {
    let line = "ab".repeat(3)
}

P0037

fn main() {
    let huge = "ab".repeat(300000000)
}

fn main() {
    let small = "ab".repeat(3000)
}

Errors and traits

Capabilities

main receives exactly the capabilities its parameters declare, and an Args parameter receives the program's arguments: args.get(0) is the program path, and the arguments after -- follow. A capability is a runtime value that carries its attenuation state, so attenuation narrows authority at runtime as well as in the types.

Scopes and tasks

scope |s| { ... } runs tasks one at a time, in the order they were spawned, so the same program gives the same result on every run.

Tests

oskac test file.osk checks the file, refuses it as oskac run would (by the checker's diagnostics, or by E0371 or E0380, for its functions and its tests), and then runs every test block in source order. A refused file runs no test.

Report and exit codes

Without --format=json, one line per test, then the failures, then a summary:

test adds ... ok
test divides ... FAILED
test reads the real config ... skipped (#[integration]; run with --integration)

failures:
test divides: math.osk: error[P0011]: assertion failed: `actual == expected`: actual 2, expected 3 (bytes 120..141)

3 tests: 1 passed, 1 failed, 1 skipped

Each failure is named by its test. Control characters in test names and failure messages are escaped (\n, \r, \t, \u{..}), so a message cannot forge a line of the report.

Output. What a test writes to stderr, dbg included, goes to the real stderr as it happens, each line prefixed with the test's name in brackets, such as [divides] [dbg] 4. What it prints to t.stdout is recorded for t.printed(), for integration tests too, so the report is the only thing on stdout.

With --format=json, one JSON object on stdout. Each test has its name, its status (passed, failed, or skipped), and its failure, a diagnostic object or null. A refused file has no tests and its diagnostics in diagnostics:

{"tests":[{"name":"adds","status":"passed","failure":null},{"name":"divides","status":"failed","failure":{"code":"P0011","message":"...","span":{"start":120,"end":141}}}],"passed":1,"failed":1,"skipped":0,"diagnostics":[]}
Exit codeMeaning
0No test failed. Skipped tests do not count.
1A test failed, or the checker refused the file.
2The file uses something the interpreter cannot run yet (E0371, E0380). No test ran.