aeneasverif / charon Goto Github PK
View Code? Open in Web Editor NEWInterface with the rustc compiler for the purpose of program verification
License: Apache License 2.0
Interface with the rustc compiler for the purpose of program verification
License: Apache License 2.0
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
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
.
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")
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.
For now Charon does not support quantified lifetimes, as indicated by for <'a> ...
in the where clauses.
This issue will probably require #63
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
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
.
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.
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.
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.
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
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.
As suggested here, to disambiguate with ItemMeta
.
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).
The case ForeigMod
is not handled by names_utils::extended_def_id_to_name
For now, quantified where clauses like below are not supported:
where for<'a> Foo : Bar<'a>
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!();
}
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>,
...
}
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.
We want to be able to run cargo charon
This is particularly important for --extract-opaque-bodies
which crashes on quite a few std
things.
We need to extract visibility information like pub
or pub(crate)
, etc.
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
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
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 }
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.
This issue tracks language features we don't support yet.
dyn Trait
: #123for<'a>
bounds: #79enum as isize
casting: #91Drop
semantics: #152vec![...]
macro: #165In workspaces the target
directory is not in the same directory as the crate. So this will always fail.
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")
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.
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.
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
This generates an error:
const S: &str = "Hello";
Error:
Unsupported constant: "ConstValue::Slice: Slice { data: ConstAllocation { .. }, start: 0, end: 98 }"
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.
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
.
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.
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!
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
charon/charon-ml/src/TypesUtils.ml
Line 209 in a0c861c
The comment should explain why we keep the function:
true
) but we might want to do something more precise in the future.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:
A note about this piece of code:
charon/charon/src/translate_functions_to_ullbc.rs
Lines 1308 to 1366 in 99e3013
Right now, there are two code-paths for translating data types constructor applications.
AggregateKind::Adt
which takes a type identifier, followed by a variant identifierOption
, 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?
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)
For cases like in #107 where a pass fails.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.