L3 semi-working (sans INVOKENATIVE)

src/bytecode/execute.ts

@@ -1,11 +1,11 @@
 import { Instruction, Program } from "./high-level";
-import { ArithmeticError, NonterminationError } from "../error";
+import { AbortError, ArithmeticError, NonterminationError } from "../error";
 
 export type Value =
     | string // runtime value of type string
     | number // runtime value of type int [-2^31, 2^31)
     //                       char [2^31, 2^31 + 128)
-    //                       bool -Infinity, Infinity
+    //                       bool -Infinity (false), Infinity (true)
     | null // void*, function pointer, regular pointer
     | { tag: "pointer"; value: Value } // non-null regular pointer
     | { tag: "function"; value: string } // non-null function pointer
@@ -50,9 +50,12 @@ export function execute(prog: Program, gas?: number): Value {
 
 export function step(prog: Program, state: State): undefined | Value {
     //console.log(state.bytecode[state.pc]);
-    //console.log(state.callstack);
+    //console.log(state.callstack.map(frame => frame.locals));
     //console.log(state.stack);
-    const instr = state.bytecode[state.pc];
+
+    // Edge case: if the PC ends up at state.bytecode.length, return
+    // The stack will be empty, but the returned "undefined" will be ignored
+    const instr: Instruction = state.pc === state.bytecode.length ? {tag: "RETURN"} : state.bytecode[state.pc];
     state.pc += 1;
     switch (instr.tag) {
         case "RETURN": {
@@ -221,6 +224,9 @@ export function step(prog: Program, state: State): undefined | Value {
             state.pc = state.labels.get(instr.argument)!;
             return undefined;
         }
+        case "ABORT": {
+            throw new AbortError(instr.argument, state.stack.pop() as string);
+        }
         case "INVOKESTATIC": {
             const f = prog.function_pool.get(instr.argument)!;
             const locals = new Map<string, Value>();

src/bytecode/generate.ts

@@ -458,12 +458,18 @@ function statement(
             const labelExit = label("while_exit");
             const invariants = contracts
                 ? stm.invariants.reduce<Instruction[]>(
-                      (instrs, exp) =>
-                          instrs
-                              .concat(expression(exp))
-                              .concat([{ tag: "ASSERT", argument: "loop_invariant" }]),
-                      []
-                  )
+                      (instrs, exp, i) => {
+                        const labelInvariantGood = label(`while_invariant_${i}_ok`);
+                        const labelInvariantFail = label(`while_invariant_${i}_fail`);
+                        return instrs
+                            .concat(conditional(exp, labelInvariantGood, labelInvariantFail))
+                            .concat([{ tag: "LABEL", argument: labelInvariantFail }])
+                            .concat([{tag: "SPUSH", argument: "loop invariant failed"}])
+                            .concat([{ tag: "ABORT", argument: "loop_invariant" }])
+                            .concat([{ tag: "LABEL", argument: labelInvariantGood }])
+                    },
+                    []
+                )
                 : [];
 
             return [{ tag: "LABEL", argument: labelStart } as Instruction]
@@ -481,10 +487,16 @@ function statement(
             const labelExit = label("for_end");
             const invariants = contracts
                 ? stm.invariants.reduce<Instruction[]>(
-                      (instrs, exp) =>
-                          instrs
-                              .concat(expression(exp))
-                              .concat([{ tag: "ASSERT", argument: "loop_invariant" }]),
+                      (instrs, exp, i) => {
+                          const labelInvariantGood = label(`for_invariant_${i}_ok`);
+                          const labelInvariantFail = label(`for_invariant_${i}_fail`);
+                          return instrs
+                              .concat(conditional(exp, labelInvariantGood, labelInvariantFail))
+                              .concat([{ tag: "LABEL", argument: labelInvariantFail }])
+                              .concat([{tag: "SPUSH", argument: "loop invariant failed"}])
+                              .concat([{ tag: "ABORT", argument: "loop_invariant" }])
+                              .concat([{ tag: "LABEL", argument: labelInvariantGood }])
+                      },
                       []
                   )
                 : [];
@@ -510,8 +522,14 @@ function statement(
                 []
             );
         case "AssertStatement": {
+            const assertBad = label("assert_fail");
+            const assertGood = label("assert_pass");
             if (!contracts && stm.contract) return [];
-            return expression(stm.test).concat([{ tag: "ASSERT", argument: stm.contract ? "assert" : null }]);
+            return conditional(stm.test, assertGood, assertBad)
+                .concat([ {tag: "LABEL", argument: assertBad }])
+                .concat([{tag: "SPUSH", argument: "assert failed"}])
+                .concat([{ tag: "ABORT", argument: stm.contract ? "assert" : null }])
+                .concat([{tag: "LABEL", argument: assertGood }])
         }
         case "ErrorStatement":
             return expression(stm.argument).concat([{ tag: "ATHROW" }]);

src/bytecode/high-level.ts

@@ -43,7 +43,7 @@ export type Instruction =
     | { tag: "IF_CCMPLE"; argument: string }
     | { tag: "GOTO"; argument: string }
     | { tag: "ATHROW" }
-    | { tag: "ASSERT"; argument: null | "assert" | "requires" | "ensures" | "loop_invariant" }
+    | { tag: "ABORT"; argument: null | "assert" | "requires" | "ensures" | "loop_invariant" }
 
     // Functions
     | { tag: "INVOKESTATIC"; argument: string }
@@ -89,8 +89,8 @@ export function instructionToString(instr: Instruction): string {
     switch (instr.tag) {
         case "LABEL":
             return `.${instr.argument}:`;
-        case "ASSERT":
-            return `   ASSERT${instr.argument ? "" : ` (${instr.argument})`}`;
+        case "ABORT":
+            return `   ABORT${instr.argument === null ? "" : ` (${instr.argument})`}`;
         case "POSITION":
             return `   ---`;
         case "VLOAD":

src/error.ts

@@ -39,6 +39,14 @@ export class NonterminationError extends Error {
     }
 }
 
+export class AbortError extends Error {
+    public readonly name: "AbortError";
+    constructor(source: null | "assert" | "requires" | "ensures" | "loop_invariant", msg: string) {
+        super(msg + (source === null ? "" : ` (@${source})`));
+        this.name = "AbortError";
+    }
+}
+
 export class ArithmeticError extends Error {
     public readonly name: "ArithmeticError";
     constructor(msg: "division by zero" | "out-of-bounds division" | "shift out of range") {

src/test/suite_test.ts

@@ -11,7 +11,7 @@ import "mocha";
 import { program } from "../bytecode/generate";
 import { Program } from "../bytecode/high-level";
 import { execute } from "../bytecode/execute";
-import { NonterminationError, ArithmeticError } from "../error";
+import { NonterminationError, ArithmeticError, AbortError } from "../error";
 
 function extractTypedefs(decls: ast.Declaration[]): Set<string> {
     return decls.reduce((set, decl) => {
@@ -129,6 +129,16 @@ function testfile(filenameLang: Lang, libs: string[], filepath: string) {
                         throw new ArithmeticError("division by zero");
                     }
                 }).to.throw(ArithmeticError);
+            } else if (spec.outcome === "abort") {
+                expect(() => {
+                    try {
+                        return execute(bytecode!, 10000000);
+                    } catch (err) {
+                        if (err.name !== "NonterminationError") throw err;
+                        console.log(err.name);
+                        throw new AbortError(null, "");
+                    }
+                }).to.throw(AbortError);
             } else if (spec.outcome === "infloop") {
                 expect(() => execute(bytecode!,  1000000)).to.throw(NonterminationError);
             } else {
@@ -140,7 +150,7 @@ function testfile(filenameLang: Lang, libs: string[], filepath: string) {
 
 const dir = "./tests";
 //readdirSync(dir).
-["l3-basic"].
+["l3-large"].
 forEach(subdir => {
     if (lstatSync(join(dir, subdir)).isDirectory()) {
         describe(`Tests in suite ${subdir}`, () => {