aeneasverif/charon

Interface with the rustc compiler for the purpose of program verification

charon's Issues

Add support for iter next

Filing this tracking issue for unsupported predicates with bound regions.

This is an example program that triggers the issue:

fn main() {
    let a = [1, 2, 3];
    let _x = a.iter().next();
}

$ charon
   Compiling any v0.1.0 (/home/ubuntu/examples/aeneas/any)
error: Predicates with bound regions (i.e., `for<'a> ...`) are not supported yet
   --> /home/ubuntu/.rustup/toolchains/nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:131:1
    |
131 | / iterator! {struct Iter -> *const T, &'a T, const, {/* no mut */}, {
132 | |     fn is_sorted_by<F>(self, mut compare: F) -> bool
133 | |     where
134 | |         Self: Sized,
...   |
138 | |     }
139 | | }}
    | |__^
    |
    = note: this error originates in the macro `iterator` (in Nightly builds, run with -Z macro-backtrace for more info)

error: Ignoring the following function due to an error: DefId(2:42967 ~ core[6c80]::slice::iter::{impl#181}::find)
   --> /home/ubuntu/.rustup/toolchains/nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:131:1
    |
131 | / iterator! {struct Iter -> *const T, &'a T, const, {/* no mut */}, {
132 | |     fn is_sorted_by<F>(self, mut compare: F) -> bool
133 | |     where
134 | |         Self: Sized,
...   |
138 | |     }
139 | | }}
    | |__^
    |
    = note: this error originates in the macro `iterator` (in Nightly builds, run with -Z macro-backtrace for more info)

error: Predicates with bound regions (i.e., `for<'a> ...`) are not supported yet
   --> /home/ubuntu/.rustup/toolchains/nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:135:12
    |
135 |         F: FnMut(&Self::Item, &Self::Item) -> Option<Ordering>,
    |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: Ignoring the following function due to an error: DefId(2:42977 ~ core[6c80]::slice::iter::{impl#181}::is_sorted_by)
   --> /home/ubuntu/.rustup/toolchains/nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:132:5
    |
132 | /     fn is_sorted_by<F>(self, mut compare: F) -> bool
133 | |     where
134 | |         Self: Sized,
135 | |         F: FnMut(&Self::Item, &Self::Item) -> Option<Ordering>,
    | |_______________________________________________________________^

error: The external definition DefId(2:42977 ~ core[6c80]::slice::iter::{impl#181}::is_sorted_by) triggered errors. It is (transitively) used at the following location(s):
 --> src/main.rs:3:14
  |
3 |     let _x = a.iter().next();
  |              ^^^^^^^^^^^^^^^

error: The external definition DefId(2:42967 ~ core[6c80]::slice::iter::{impl#181}::find) triggered errors. It is (transitively) used at the following location(s):
 --> src/main.rs:3:14
  |
3 |     let _x = a.iter().next();
  |              ^^^^^^^^^^^^^^^

[ INFO charon_driver::export:101] [gexport]: Generated the partial (because we encountered errors) file: /home/ubuntu/examples/aeneas/any/any.llbc
[ ERROR charon_driver:231] The extraction encountered 4 errors
error: could not compile `any` (bin "any") due to 6 previous errors

Binary location

README.md says the charon executable is located at bin/charon. On my machine, I found it at charon/target/debug/charon. I am using OSX, and built charon using gmake build-charon-rust.

Add support for mutually recursive trait definitions

Mutually recursive traits happen in practice, for example here (mutual recursion between PrimeField and Field):

pub trait Trait1 {
    type T: Trait2;
}

pub trait Trait2: Trait1 {}

It would be good to handle those, or at least print a nice error message. For now, Charon panics with:

thread 'rustc' panicked at 'Invalid trait decl group:
tests4::Trait1
tests4::Trait2', src/reorder_decls.rs:116:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: could not compile `tests4` (bin "tests4")

Non-positive indexes for variants are unhandled

Consider:

enum Ordering {
    Lesser  = -1,
    Equal = 0,
    Greater = 1
}

(taken from https://github.com/RaitoBezarius/avl-verification/blob/main/src/main.rs)

Charon will crash because it will generate a usize::MAX - 1 > u32::MAX for https://github.com/RaitoBezarius/avl-verification/blob/main/src/main.rs#L29 variant in the pattern matching.

Add support for quantified lifetimes (`for <'a>`)

For now Charon does not support quantified lifetimes, as indicated by for <'a> ... in the where clauses.

Extract inlining information

This issue will probably require #63

Add support for `dyn Trait`

Retrieve the result of drop elaboration

Error with a generic const

For the following Rust program:

struct Foo<T> {
    x: Option<T>,
}

impl<T> Foo<T> {
    const FOO: Result<T, i32> = Err(0);
}

charon errors out:

$ charon
   Compiling const_gen v0.1.0 (/home/ubuntu/examples/aeneas/const_gen)
error: Could not find the type variable "T" (index: 0)
 --> src/main.rs:6:5
  |
6 |     const FOO: Result<T, i32> = Err(0);
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^

error: Ignoring the following global due to an error: DefId(0:8 ~ const_gen[4689]::{impl#0}::FOO)
 --> src/main.rs:6:5
  |
6 |     const FOO: Result<T, i32> = Err(0);
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^

[ INFO charon_driver::export:101] [gexport]: Generated the partial (because we encountered errors) file: /home/ubuntu/examples/aeneas/const_gen/const_gen.llbc
[ ERROR charon_driver:231] The extraction encountered 2 errors
error: could not compile `const_gen` (bin "const_gen") due to 2 previous errors

Update the CI to format the code and check that there are no compilation warnings

Use a `Vec` in `RawStatement::Sequence`

Currently it takes a pair of statements, which isn't very practical to pattern-match on. If it was a Vec, we could use slice patterns which should be a lot more convenient.

The drawback is we can't move out of a slice pattern, so we'll either have to clone or insert/remove on the Vec.

Reorganize the Charon files into subfolders

Dependency lookup is broken

It looks like the dependency lookup isn't implementing the -/_ replacement in crate names and thus can't find dependencies with a - in the name.

https://github.com/Kachoc/charon/blob/7154478ad283b2a8b5fc4a409187c86137505223/charon/src/main.rs#L464

Compilation hangs when having a type defined inside a trait

The following code snippet

pub trait Trait1 {
    type T: Trait2;
}

pub trait Trait2: Trait1 {
    type U;
}

makes charon hang. The motivation for this structure can be found in arkworks/ff.

Add an option to extract the bodies of the external definitions

For now, whenever possible we treat foreign definitions as opaque, that is we treat all external functions as opaque and thus don't look at their bodies, treat external structures without public fields as opaque, etc. It is sometimes useful to extract the bodies of the external definitions, and Eurydice needs this: we need to add a CLI option for this. Also, it might be good to be able to tweak this behavior, for instance by extracting only the bodies of the functions marked as #[inline], etc.

Misc issues (map, const generic, array updates, assertions)

Here are some issues when trying to run charon on Rust code.

map

pub fn map(x: [i32; 256],) -> [i32; 256] {
    x.map(|v| v)
}

thread 'rustc' panicked at 'not implemented: impl source: ImplSourceClosureData(closure_def_id=DefId(0:6 ~ simplemap[2625]::add::{closure#0}), substs=[i16, extern "rust-call" fn((i32,)) -> i32, ()], nested=[Obligation(predicate=Binder(ClosureKind(DefId(0:6 ~ simplemap[2625]::add::{closure#0}), [i16, extern "rust-call" fn((i32,)) -> i32, ()], FnMut), []), depth=1)])', /Users/franziskus/.cargo/git/checkouts/hacspec-v2-fad44c11f2620bcb/60ef8f9/frontend/exporter/src/types/traits.rs:428:13

const generic

pub fn array<const LEN: usize>() -> [u8; LEN] {
    [0u8; LEN]
}

thread 'rustc' panicked at 'internal error: entered unreachable code: ConstGeneric::as_value: Not the proper variant', src/types.rs:404:56

array update in loops

fn cbd(mut prf_input: [u8; 33]) {
    for i in 0..3 {
        prf_input[0] = i;
    }
}

thread 'rustc' panicked at 'internal error: entered unreachable code: Could not find a clause for parameter:
- target param: @TraitDecl1<Self::IntoIter>
- available clauses:
@TraitDecl0<Self>', src/translate_predicates.rs:599:13

assertions

pub(crate) fn select(lhs: &[u8], rhs: &[u8]) {
    debug_assert_eq!(lhs.len(), rhs.len());
}

thread 'rustc' panicked at 'Unsupported ADT: core::panicking::AssertKind', src/translate_functions_to_ullbc.rs:924:33

Add support for attributes

It would be good to have the possibility of annotating the Rust definitions with attributes, for instance to mark some definitions as opaque, to tweak the name of the definitions for the extraction, etc.

Rename `Meta` to `SpanMeta`

As suggested here, to disambiguate with ItemMeta.

Check in CI that the build doesn't generate warnings

It can happen that the compilation generates warnings (for instance, clippy warnings): I want to make sure it doesn't happen (i.e., all warnings are addressed before we merge).

Def Ids: handle the case `ForeignMod`

The case ForeigMod is not handled by names_utils::extended_def_id_to_name

Add support for quantified where clauses (`for <'a>`)

For now, quantified where clauses like below are not supported:

where for<'a> Foo : Bar<'a>

panic in empty function

Getting the length of a slice is not supported.

pub fn some_error(_: &[u8]) {}

produces

[15:00:25 TRACE charon::translate_functions_to_im:2037] [translate_function_signature]:
# Output variable type:
()
thread 'rustc' panicked at 'not implemented', src/regions_hierarchy.rs:352:13

Note that Charon is fine with the following

pub fn no_error() {}

I think a lot of the issues are stemming from the same issue that array and slices aren't supported (regions_hierarchy.rs).

        Ty::Array(_aty) => {
            unimplemented!();
        }
        Ty::Slice(_sty) => {
            unimplemented!();
        }

Support `Rvalue::Discriminant` not followed by `SwitchInt`

This can show up in optimized MIR, for example the optimized mir of Option::is_some(). It's not too hard to support: we can replace _x = Discriminant(_y) with

match _y {
    Variant1 => _x = <discriminant value for variant 1>,
    ...
}

Make the ScalarValue::Isize and Usize variants use i64 and u64 instead of isize/usize

In values.rs we have:

pub enum ScalarValue {
    Isize(isize),
    Usize(usize),
    ...
}

This doesn't work if we do cross-compilation: we should use i64 and u64 to store the integer values.

Turn charon into a subcommand

We want to be able to run cargo charon

Gracefully fail when failing to extract a body

This is particularly important for --extract-opaque-bodies which crashes on quite a few std things.

Extract visibility information

We need to extract visibility information like pub or pub(crate), etc.

Support enum-to-discriminant casting

For the following program:

enum Foo {
    A,
    B,
}

fn main() {
    let x = Foo::A;
    let _y = x as isize;
}

Charon errors out:

$ charon
   Compiling discr v0.1.0 (/home/ubuntu/examples/aeneas/discr)
error: Unsupported statement kind: intrinsic
 --> src/main.rs:8:14
  |
8 |     let _y = x as isize;
  |              ^^^^^^^^^^

[ INFO charon_driver::export:101] [gexport]: Generated the partial (because we encountered errors) file: /home/ubuntu/examples/aeneas/discr/discr.llbc
[ ERROR charon_driver:231] The extraction encountered 1 errors
error: could not compile `discr` (bin "discr") due to previous error

Traits breaks Charon

Using the Debug or Clone trait breaks Charon. Looking at the code that fails I expect that any trait will make Charon panic really.

pub fn trait_error(s: &[u8]) {
  let _array: [u8; 4] = s.try_into().unwrap();
}

produces the following error (try_into requires implementation of Debug).

[13:34:02 TRACE charon::generics:105] [check_generics]:
trait_name: core::fmt::Debug
thread 'rustc' panicked at 'assertion failed: trait_name.equals_ref_name(&assumed::MARKER_SIZED_NAME)', src/generics.rs:106:17

Similarly,

pub fn vec_error() {
  let _vec = vec![0u8; 5];
}

produces

[13:46:49 TRACE charon::generics:105] [check_generics]:
trait_name: core::clone::Clone
thread 'rustc' panicked at 'assertion failed: trait_name.equals_ref_name(&assumed::MARKER_SIZED_NAME)', src/generics.rs:106:17

Hide associated types equality constraints

The following is unsupported because we don't handle the equality constraint:

trait Iterator {
    type Item;
}

fn f<I, J>(x: I::Item) -> J::Item
where
    I: Iterator,
    J: Iterator<Item=I::Item>,
{ x }

The solution proposed by @sonmarcho would be to transform associated types into type parameters. Type equalities would then only apply to free type variables, which we can handle by merging the identical variables. We would therefore generate:

trait Iterator<Item> {}

fn f<I, J, Item>(x: Item) -> Item
where
    I: Iterator<Item>,
    J: Iterator<Item>,
{ x }

Detect overflow checks properly

After #124, there's still a case where we don't detect overflow checks properly:

fn div_signed_with_constant() -> i32 {
    const FOO: i32 = 42;
    FOO / 2
}

gives:

fn test_crate::div_signed_with_constant() -> i32
{
    let @0: i32; // return
    let @1: bool; // anonymous local
    let @2: bool; // anonymous local
    let @3: i32; // anonymous local
    let @4: i32; // anonymous local

    @1 := const (2 : i32) == const (-1 : i32)
    @3 := test_crate::div_signed_with_constant::FOO
    @2 := move (@3) == const (-2147483648 : i32)
    @4 := test_crate::div_signed_with_constant::FOO
    @0 := move (@4) / const (2 : i32)
    return
}

because the constants are inserted in the middle of the checks.

Tracking issue for unsupported rust features

This issue tracks language features we don't support yet.

Planned

• dyn Trait: #123
• for<'a> bounds: #79
• String constants: #72
• enum as isize casting: #91
• pre-/post-conditions and invariants: #64
• Retain type aliases: #134
• Transform associated type equalities into definitional equalities: #127
• Mutually recursive traits: #94
• Emit provided trait methods differently: AeneasVerif/aeneas#70
• Correct Drop semantics: #152
• vec![...] macro: #165

Not planned at the moment

• Unsafe code
• Remove overflow checks in CTFE code (i.e. constants)

Doesn't support workspaces

In workspaces the target directory is not in the same directory as the crate. So this will always fail.

https://github.com/Kachoc/charon/blob/7154478ad283b2a8b5fc4a409187c86137505223/charon/src/main.rs#L405

`assertion failed: int_ty.is_isize()` when deriving `PartialOrd`

For the following program:

#[derive(PartialEq, PartialOrd)]
struct Foo {
    x: i32,
    y: i32,
}

fn main() { }

charon crashes as follows:

$ RUST_BACKTRACE=1 charon
   Compiling ord v0.1.0 (/home/ubuntu/examples/aeneas/ord)
thread 'rustc' panicked at 'assertion failed: int_ty.is_isize()', src/remove_read_discriminant.rs:56:17
stack backtrace:
   0: rust_begin_unwind
             at /rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/std/src/panicking.rs:593:5
   1: core::panicking::panic_fmt
             at /rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/panicking.rs:67:14
   2: core::panicking::panic
             at /rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/panicking.rs:117:5
   3: charon_driver::remove_read_discriminant::Visitor::update_statement
   4: charon_driver::llbc_ast_utils::MutAstVisitor::default_visit_raw_statement
   5: charon_driver::llbc_ast_utils::MutAstVisitor::default_visit_raw_statement
   6: charon_driver::translate_ctx::TransCtx::iter_bodies
   7: charon_driver::driver::translate
   8: <charon_driver::driver::CharonCallbacks as rustc_driver_impl::Callbacks>::after_parsing
   9: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
  10: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_span::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
error: could not compile `ord` (bin "ord")

Remove the ULLBC

Allow selecting packages within workspaces

Currently Charon appears to parse the entire workspace instead of the package in the current directory.

When executing charon in a member of a workspace I'd expect it to operate only on this crate. hax allows specifying packages and only uses the current crate.

Consider adding version numbers in the .llbc files

Right now, charon-ml might fail to load a .llbc file because, say, charon produces a new construct, but charon-ml does not (yet) know how to read it. Or, worse, a .llbc file is stale (old), and charon-ml is recent, and the .llbc file has not been regenerated properly, which means that there is a version mismatch.

Version numbers might help providing a useful error message, and figure out the discrepancy.

from_le_bytes not usable

Trying to convert u8 to u32 breaks.

pub fn builtin_error(s: [u8; 4]) {
  let _value = u32::from_le_bytes(s);
}

produces

[13:37:11 TRACE charon::names_utils:124] [item_def_id_to_name]:
DefId(2:25039 ~ core[1586]::num::{impl#8}::from_le_bytes)
thread 'rustc' panicked at 'internal error: entered unreachable code', src/names_utils.rs:230:25

Add support for string literals

This generates an error:

const S: &str = "Hello";

Error:

Unsupported constant: "ConstValue::Slice: Slice { data: ConstAllocation { .. }, start: 0, end: 98 }"

`cargo-charon` fails to parse arguments correctly

Cargo version: cargo 1.66.0-nightly (7e484fc1a 2022-10-27)

I installed cargo-charon as a Cargo CLI extension using cargo install. Invoking cargo charon fails for me on a simple repository due to what appears to be an argument-parsing error:

error: Found argument 'charon' which wasn't expected, or isn't valid in this context

USAGE:
    cargo-charon [FLAGS] [OPTIONS]

For more information try --help

Manually running the cargo-charon executable from where Cargo installed it to works as expected.

---

I took the above approach because the executable is named like a Cargo plugin, and because the documentation suggests something which no longer works (cargo run errors out due to the lack of a default executable.) If cargo-charon isn't meant to be installed like this, I'm happy to update the docs in some way.

Get rid of the Makefiles

The Makefiles are getting bloated, especially for the tests, and are hard to maintain especially for people who are not used to writing makefiles. It would be better to have a script file or, probably better, only rely on cargo.

Ignore dev-dependencies

Charon appears to expect dev-dependencies to be compiled, i.e. running cargo build is not enough.
If this is intentional, the recommendation should be changed to run cargo build --tests or a switch could be added to not look at tests.

Export type aliases in LLBC

This is particularly useful for Eurydice. I have a mechanism for picking user-provided type abbreviations, but instead end up generating things like this https://github.com/cryspen/hacl-packages/pull/457/files#diff-a94673428367ed62df2e7dd7d29ef4b6576ee2bd5e9cf33beed83e3f452e3602R106-R115 because I no longer have the information that the user had provided a custom name (much shorter) for these types.

This doesn't need to change anything else in Charon, the type abbreviations can still be inlined, it's just a matter of keeping the type alias also in scope for me to do something useful with it. Thanks!

Add support for spec annotations

It would be good to add the possibility of annotating the definitions with pre/post-conditions and even proof annotations.
This issue should be done after #63

Update the comment for `TypesUtils.ty_is_copyable`

charon/charon-ml/src/TypesUtils.ml

Line 209 in a0c861c

* traits.

The comment should explain why we keep the function:

• it is used in the code of Aeneas exactly where we need to check that a type is copyable
• for now we don't do the check (as the function always returns true) but we might want to do something more precise in the future.
• if we do so, it is good not to have to dive in the code to notice where we should reinsert the checks, because we would likely miss some

Support for for-loops

Ended up hitting this code today:

  for j in 0..256 {
    r[j] = fqmul(r[j], F);
  }

This is not currently supported because it relies on an iterator trait, and we don't support traits. Rather than do a lot of peephole optimizations in Charon to recognize this and extract it as a dedicated AST for node, we suggest:

• supporting traits, in general
• adding an optional phase in charon-ml that takes care of pattern-matching on this particular usage of traits and rewriting it into a dedicated high-level For AST node

Represent data type constructors with strings instead of variant ids

A note about this piece of code:

charon/charon/src/translate_functions_to_ullbc.rs

Lines 1308 to 1366 in 99e3013

	if adt_id.is_local() {
	// Local ADT: retrieve the definition
	let id_t = *bt_ctx.ft_ctx.ordered.type_rid_to_id.get(adt_id).unwrap();
	let def = bt_ctx.get_type_defs().get_type_def(id_t).unwrap();
	assert!(region_params.len() == def.region_params.len());
	assert!(type_params.len() == def.type_params.len());
	let variant_id = match &def.kind {
	ty::TypeDeclKind::Enum(variants) => {
	let variant_id = translate_variant_id(*variant_idx);
	assert!(
	operands_t.len()
	== variants.get(variant_id).unwrap().fields.len()
	);
	Some(variant_id)
	}
	ty::TypeDeclKind::Struct(_) => {
	assert!(variant_idx.as_usize() == 0);
	None
	}
	ty::TypeDeclKind::Opaque => {
	unreachable!("Can't build an aggregate from an opaque type")
	}
	};
	let akind =
	e::AggregateKind::Adt(id_t, variant_id, region_params, type_params);
	e::Rvalue::Aggregate(akind, operands_t)
	} else {
	// External ADT.
	// Can be `Option`
	// TODO: treat all external ADTs in a consistant manner.
	// For instance, we can access the variants of any external
	// enumeration marked as `public`.
	let name = type_def_id_to_name(tcx, *adt_id);
	assert!(name.equals_ref_name(&assumed::OPTION_NAME));
	// Sanity checks
	assert!(region_params.is_empty());
	assert!(type_params.len() == 1);
	// Find the variant
	let variant_id = translate_variant_id(*variant_idx);
	if variant_id == assumed::OPTION_NONE_VARIANT_ID {
	assert!(operands_t.is_empty());
	} else if variant_id == assumed::OPTION_SOME_VARIANT_ID {
	assert!(operands_t.len() == 1);
	} else {
	unreachable!();
	}
	let akind =
	e::AggregateKind::Option(variant_id, type_params.pop().unwrap());
	e::Rvalue::Aggregate(akind, operands_t)
	}

Right now, there are two code-paths for translating data types constructor applications.

• If we have access to the definition of the data type (it is "local"), then we look up the definition of the data type, then compute a variant id, which is essentially the index of the variant in the data type definition, and represent the constructor application as AggregateKind::Adt which takes a type identifier, followed by a variant identifier
• If we do not have access to the definition of the data type (it is not local), then it must be one of the few built-in types we know how to handle. One such type is Option, for which we hardwire the knowledge that the VariantId of None is 0, and that the VariantId of Some is 1. (My most recent PR adds Range as another builtin type.)

The main issue with this translation scheme is that we cannot handle non-local (a.k.a. opaque) types in a generic fashion, because we need that map from constructor to VariantId.

A possible solution (to be discussed) is to represent variants with mere names (i.e., strings), which would then allow for a single translation scheme, regardless of whether the definition is available or not.

@sonmarcho do you remember why VariantId's are important?

Add span information to structure fields, trait items, etc.

Tracking issue for not crashing on the rustc test suite

In #136 we added a script that runs charon on the rustc test suite and displays the results. As we'd like to support a large portion of the rust language, we track in this issue our results on these tests.

Our first aim is to never panic. Initial results:

   5269 expected-failure
   2585 failure
   3105 panic
   4207 success
     27 timeout

(Please don't post on this conversation, it's mean for automated posting)

Add `StatementKind::Error`

For cases like in #107 where a pass fails.