Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Assertions and irrecoverable runtime errors #158

Merged
merged 9 commits into from
Dec 15, 2024
Merged

Assertions and irrecoverable runtime errors #158

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
3302f72
Assertions and irrecoverable runtime errors
ppolesiuk Nov 22, 2024
f43a86e
Merge branch 'master' into 157-irrecoverable-errors
ppolesiuk Nov 22, 2024
46453dc
Runtime error as a special exception
ppolesiuk Nov 25, 2024
cef6ac9
Merge branch 'master' into 157-irrecoverable-errors
forell Dec 12, 2024
18b0324
Use new comment syntax in Assert
forell Dec 12, 2024
01ac2d7
Add `unwrap*` methods for `Option` and some tweaks
forell Dec 13, 2024
81ce2c5
Merge branch 'master' into 157-irrecoverable-errors
forell Dec 15, 2024
7aacb27
Add `unwrapErr` method to `Option`
forell Dec 15, 2024
ff8cb6a
Rename test
forell Dec 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 28 additions & 0 deletions lib/Base/Assert.fram
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
(* This file is part of DBL, released under MIT license.
* See LICENSE for details.
*)

import open Types

(** Abort the program with given message.

Note that this function is pure. In correct programs, this function should
be never called at runtime, but it can be used to appease the type-checker.
Use this function only in impossible match clauses or in case of gross
violation of function preconditions (e.g., division by zero). *)
pub let runtimeError {type T} =
(extern dbl_runtimeError : String ->[] T)

(** Explicitly assert, that this case is impossible *)
pub let assertImpossible {?msg : String} () =
ppolesiuk marked this conversation as resolved.
Show resolved Hide resolved
runtimeError
match msg with
| None => "Assertion failed"
| Some msg => msg
end

(** Assert, that given condition should always hold. *)
pub let assert {?msg} b =
if b then ()
else
assertImpossible {?msg} ()
13 changes: 7 additions & 6 deletions lib/Base/Int.fram
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

import open Types
import open Operators
import open Assert

pub method toString = (extern dbl_intToString : Int -> String) self
pub method toInt64 = (extern dbl_intToInt64 : Int -> Int64) self
Expand All @@ -19,13 +20,13 @@ pub method add = (extern dbl_addInt : Int -> Int -> Int) self
pub method sub = (extern dbl_subInt : Int -> Int -> Int) self
pub method mul = (extern dbl_mulInt : Int -> Int -> Int) self

pub method div {~re : {type X} -> Unit ->[|_] X} (n : Int) =
if n.equal 0 then ~re ()
else (extern dbl_divInt : Int -> Int -> Int) self n
pub method div (n : Int) =
assert {msg="Division by zero"} (n.neq 0);
(extern dbl_divInt : Int -> Int -> Int) self n
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have a philosophical question: is the type of this extern correct? Or should it be Int -> Int ->[] Int? The decision will to influence the overall type of this method (because it uses assert), but in the potential optimizing compiler can we assume that this function always terminates correctly?

The same question applies for some other function modified in this PR.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well the effect in this case doesn't come from the extern, but from assertion, so in my opinion it works both ways.


pub method mod {~re : {type X} -> Unit ->[|_] X} (n : Int) =
if n.equal 0 then ~re ()
else (extern dbl_modInt : Int -> Int -> Int) self n
pub method mod (n : Int) =
assert {msg="Division by zero"} (n.neq 0);
(extern dbl_modInt : Int -> Int -> Int) self n

pub method neg {self : Int} = 0 - self

Expand Down
21 changes: 12 additions & 9 deletions lib/Base/Int64.fram
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

import open Types
import open Operators
import open Assert

pub method equal {self : Int64} =
(extern dbl_eqInt64 : Int64 -> Int64 -> Bool) self
Expand All @@ -26,12 +27,12 @@ pub method sub {self : Int64} =
(extern dbl_subInt64 : Int64 -> Int64 -> Int64) self
pub method mul {self : Int64} =
(extern dbl_mulInt64 : Int64 -> Int64 -> Int64) self
pub method div {~re : {type X} -> Unit ->[|_] X} (n : Int64) =
if n.equal 0L then ~re ()
else (extern dbl_divInt64 : Int64 -> Int64 -> Int64) self n
pub method mod {~re : {type X} -> Unit ->[|_] X} (n : Int64) =
if n.equal 0L then ~re ()
else (extern dbl_modInt64 : Int64 -> Int64 -> Int64) self n
pub method div (n : Int64) =
assert {msg="Division by zero"} (n.neq 0L);
(extern dbl_divInt64 : Int64 -> Int64 -> Int64) self n
pub method mod (n : Int64) =
assert {msg="Division by zero"} (n.neq 0L);
(extern dbl_modInt64 : Int64 -> Int64 -> Int64) self n

pub method land = (extern dbl_andInt64 : Int64 -> Int64 -> Int64) self
pub method lor = (extern dbl_orInt64 : Int64 -> Int64 -> Int64) self
Expand All @@ -45,14 +46,16 @@ pub method pred {self : Int64} = self - 1L

pub method toString {self : Int64} =
(extern dbl_int64ToString : Int64 -> String) self
pub method toInt {~re : {type X} -> Unit ->[|_] X, self : Int64} =
pub method toIntErr { ~onError, self : Int64 } =
if self <= 0x3fffffffffffffffL && self >= 0xc000000000000000L then
(extern dbl_int64ToInt : Int64 -> Int) self
else ~re ()
(extern dbl_intToInt64 : Int64 -> Int) self
else ~onError ()
pub method toIntOpt {self : Int64} =
if self <= 0x3fffffffffffffffL && self >= 0x7fffffffffffffffL then
Some ((extern dbl_int64ToInt : Int64 -> Int) self)
else None
pub method toInt {self : Int64} =
self.toIntErr { ~onError = fn () => runtimeError "Conversion overflow" }

pub method abs {self : Int64} =
if self < 0L then self.neg else self
Expand Down
8 changes: 4 additions & 4 deletions lib/Base/String.fram
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

import open /Base/Types
import open /Base/Operators
import open /Base/Assert
import /Base/Int

pub method add = (extern dbl_strCat : String -> String -> String) self
Expand All @@ -16,10 +17,9 @@ pub method ge = (extern dbl_geStr : String -> String -> Bool) self
pub method le = (extern dbl_leStr : String -> String -> Bool) self

pub method length = (extern dbl_strLen : String -> Int) self
pub method get {~re : {type X} -> Unit ->[|_] X, self : String} (n : Int) =
if n >= 0 && n < self.length then
(extern dbl_strGet : String -> Int -> Char) self n
else ~re ()
pub method get {self : String} (n : Int) =
assert {msg="Out of bounds"} (n >= 0 && n < self.length);
(extern dbl_strGet : String -> Int -> Char) self n

pub method toList {self : String} =
let getChar = extern dbl_strGet : String -> Int -> Char in
Expand Down
2 changes: 2 additions & 0 deletions lib/Prelude.fram
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

import /Base/Types
import /Base/Operators
import /Base/Assert
import /Base/Bool
import /Base/Int
import /Base/Int64
Expand All @@ -12,6 +13,7 @@ import /Base/String

pub open Types
pub open Operators
pub open Assert

pub let id x = x

Expand Down
6 changes: 5 additions & 1 deletion src/Eval/External.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,12 @@ let int64_cmpop op = int64_fun2 (fun x y -> of_bool (op x y))

let str_cmpop op = str_fun (fun s1 -> str_fun (fun s2 -> of_bool (op s1 s2)))

let runtime_error msg =
failwith ("Runtime error: " ^ msg)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think this should be implemented using failwith. Triggering this function will result in output:

Fatal error: exception Failure("Runtime error: Assertion failed")

Personally i think it should be Just Runtime error: Assertion failed, so this code should be changed to eprintf + exit 1

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would add possibility to add custom error code/number on exit.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree that this error should not be implemented with failwith. Maybe a custom exception that is handled in the main file would be better? The REPL implementation could catch this exception and recover with a prompt for an another command, instead of aborting the interpreter.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually that would probably be best

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know and possible I am wrong but this sounds like an error implementation which we would make in standard library.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you mean the issue #130? I think these two are two different things. In this PR we talk about errors that should never occur in correct programs (but unfortunately, most of programs are incorrect), so the effect of such error is pure ([]). In #130 the error has some effect visible in types. However, after merging this PR, we may rethink if we still want to implement #130.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

However, I realized that catching runtime error in REPL is not as trivial as I thought. It is not just adding extra match clasue in Eval.ml, because the exception are catch before the evaluation. I think it is still possible to handle it correctly, because the evaluator is in CPS, but it would be a more complex change, and should be done in a separate issue.


let extern_map =
[ "dbl_negInt", int_unop ( ~- );
[ "dbl_runtimeError", str_fun runtime_error;
"dbl_negInt", int_unop ( ~- );
"dbl_addInt", int_binop ( + );
"dbl_subInt", int_binop ( - );
"dbl_mulInt", int_binop ( * );
Expand Down