Generated rust code doesn't compile

womeier commented 7 months ago

I'm trying to extract the CertiCoq benchmarks to rust and run them. The extraction succeeds for all of them, but not all of them compile.

What works

demo1, demo2, list_sum (these are fairly small)
binom (works with export RUST_MIN_STACK=1000000000 otherwise the rust compiler crashes, see https://github.com/rust-lang/rust/issues/122715)
color (some Wasm tools have issues with the Wasm file our CertiCoq-Wasm generates for color, but no issues with the rust extraction)

What doesn't work (see compilation errors below)

vs_easy, vs_hard (seems to be the same problem)
sha_fast (seems to be a separate issue)

Rust extraction setup in one diff

see this diff

To set up yourself

clone: https://github.com/womeier/certicoqwasm/tree/rustextraction (no need to compile certicoq, the benchmarks have no dependencies other than coq-rust-extraction)
cd benchmarks && make for the extraction, runs one benchmark successfully (prints 100))
python3 run_rust_benchmarks.py, this calls cargo run for all benchmarks, which includes printing some lengthy s-expressions to stdout)

Versions

Coq: 8.17.0 MetaCoq: v1.2.1-8.17 rustc: 1.76.0 (07dca489a 2024-02-04)

coq-rust-extraction: most recent (https://github.com/AU-COBRA/coq-rust-extraction/commit/6e72e1c605102cdf4863f65e05a34676be98c0bf)

Errors

vs easy

``` cargo run Compiling vs_easy v0.1.0 (/home/wolfgang/ProjectsUni/Compilerstep/certicoqwasm-rustextraction/benchmarks/rust/vs_easy-extracted) error: expected identifier, found keyword `loop` --> src/main.rs:9667:27 | 9667 | hint_app(hint_app({ let loop = self.alloc(std::cell::Cell::new(None)); | ^^^^ expected identifier, found keyword | help: escape `loop` to use it as an identifier | 9667 | hint_app(hint_app({ let r#loop = self.alloc(std::cell::Cell::new(None)); | ++ error: expected `{`, found `.` --> src/main.rs:9668:27 | 9668 | loop.set(Some( | ----^ expected `{` | | | while parsing this `loop` expression error[E0061]: this method takes 2 arguments but 0 arguments were supplied --> src/main.rs:261:8 | 261 | self.Coq_PArith_BinPosDef_Pos_add() | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing | note: method defined here --> src/main.rs:258:4 | 258 | fn Coq_PArith_BinPosDef_Pos_add(&'a self, a: u64, b: u64) -> u64 { a + b } | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------ ------ help: provide the arguments | 261 | self.Coq_PArith_BinPosDef_Pos_add(/* u64 */, /* u64 */) | ~~~~~~~~~~~~~~~~~~~~~~ error[E0308]: mismatched types --> src/main.rs:261:3 | 260 | fn CertiCoq_Benchmarks_lib_vs_add_id(&'a self) -> &'a dyn Fn(u64) -> &'a dyn Fn(u64) -> u64 { | ----------------------------------------- expected `&'a (dyn Fn(u64) -> &'a (dyn Fn(u64) -> u64 + 'a) + 'a)` because of return type 261 | self.Coq_PArith_BinPosDef_Pos_add() | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `&dyn Fn(u64) -> &dyn Fn(u64) -> u64`, found `u64` | = note: expected reference `&'a (dyn Fn(u64) -> &'a (dyn Fn(u64) -> u64 + 'a) + 'a)` found type `u64` error[E0061]: this method takes 2 arguments but 0 arguments were supplied --> src/main.rs:302:12 | 302 | self.Coq_PArith_BinPosDef_Pos_add()( | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing | note: method defined here --> src/main.rs:258:4 | 258 | fn Coq_PArith_BinPosDef_Pos_add(&'a self, a: u64, b: u64) -> u64 { a + b } | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------ ------ help: provide the arguments | 302 | self.Coq_PArith_BinPosDef_Pos_add(/* u64 */, /* u64 */)( | ~~~~~~~~~~~~~~~~~~~~~~ error[E0618]: expected function, found `u64` --> src/main.rs:302:7 | 302 | self.Coq_PArith_BinPosDef_Pos_add()( | -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;` | _______| | | 303 | | p)( | |__________- call expression requires function error[E0061]: this method takes 2 arguments but 0 arguments were supplied --> src/main.rs:509:16 | 509 | self.Coq_PArith_BinPosDef_Pos_compare()( | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing | note: method defined here --> src/main.rs:383:4 | 383 | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::Ordering { | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------ ------ help: provide the arguments | 509 | self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)( | ~~~~~~~~~~~~~~~~~~~~~~ error[E0618]: expected function, found `std::cmp::Ordering` --> src/main.rs:509:11 | 509 | self.Coq_PArith_BinPosDef_Pos_compare()( | -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;` | ___________| | | 510 | | v)( | |______________- call expression requires function error[E0061]: this method takes 2 arguments but 0 arguments were supplied --> src/main.rs:784:14 | 784 | match self.Coq_PArith_BinPosDef_Pos_compare()( | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing | note: method defined here --> src/main.rs:383:4 | 383 | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::Ordering { | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------ ------ help: provide the arguments | 784 | match self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)( | ~~~~~~~~~~~~~~~~~~~~~~ error[E0618]: expected function, found `std::cmp::Ordering` --> src/main.rs:784:9 | 784 | match self.Coq_PArith_BinPosDef_Pos_compare()( | -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;` | _________| | | 785 | | self.CertiCoq_Benchmarks_lib_vs_clause_prio( 786 | | cl1))( | |_________________- call expression requires function error[E0061]: this method takes 2 arguments but 0 arguments were supplied --> src/main.rs:2689:18 | 2689 | match self.Coq_PArith_BinPosDef_Pos_compare()( | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing | note: method defined here --> src/main.rs:383:4 | 383 | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::Ordering { | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------ ------ help: provide the arguments | 2689 | match self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)( | ~~~~~~~~~~~~~~~~~~~~~~ error[E0618]: expected function, found `std::cmp::Ordering` --> src/main.rs:2689:13 | 2689 | match self.Coq_PArith_BinPosDef_Pos_compare()( | -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;` | _____________| | | 2690 | | i)( | |________________- call expression requires function error[E0308]: mismatched types --> src/main.rs:3765:29 | 3762 | self.CertiCoq_Benchmarks_lib_vs_mergeC( | --------------------------------- arguments to this method are incorrect ... 3765 | / self.Coq_Init_Datatypes_id()( 3766 | | ()), | |_________________________________^ expected `&dyn Fn(&...) -> ...`, found `&dyn Fn(())` | = note: expected reference `&dyn Fn(&CertiCoq_Benchmarks_lib_vs_expr<'_>) -> &CertiCoq_Benchmarks_lib_vs_expr<'_>` found reference `&dyn Fn(())` note: method defined here --> src/main.rs:3658:4 | 3658 | fn CertiCoq_Benchmarks_lib_vs_mergeC(&'a self, A_cmp: &'a dyn Fn(A) -> &'a dyn Fn(A) -> std::cmp::Ordering, B_cmp: &'a dyn Fn(B) -> &'a dyn Fn(B) -> std::cmp::Ordering, fAB: &'a dyn Fn(A) -> B, a... | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ----------------------- error[E0061]: this method takes 2 arguments but 0 arguments were supplied --> src/main.rs:6533:10 | 6533 | self.Coq_PArith_BinPosDef_Pos_compare()( | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing | note: method defined here --> src/main.rs:383:4 | 383 | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::Ordering { | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------ ------ help: provide the arguments | 6533 | self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)( | ~~~~~~~~~~~~~~~~~~~~~~ error[E0618]: expected function, found `std::cmp::Ordering` --> src/main.rs:6533:5 | 6533 | self.Coq_PArith_BinPosDef_Pos_compare()( | -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;` | _____| | | 6534 | | i)( | |________- call expression requires function Some errors have detailed explanations: E0061, E0308, E0618. For more information about an error, try `rustc --explain E0061`. error: could not compile `vs_easy` (bin "vs_easy") due to 15 previous errors ```

vs hard

``` running: vs_hard Compiling vs_hard v0.1.0 (/home/wolfgang/ProjectsUni/Compilerstep/certicoqwasm-rustextraction/benchmarks/rust/vs_hard-extracted) error[E0061]: this method takes 2 arguments but 0 arguments were supplied --> src/main.rs:261:8 | 261 | self.Coq_PArith_BinPosDef_Pos_add() | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing | note: method defined here --> src/main.rs:258:4 | 258 | fn Coq_PArith_BinPosDef_Pos_add(&'a self, a: u64, b: u64) -> u64 { a + b } | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------ ------ help: provide the arguments | 261 | self.Coq_PArith_BinPosDef_Pos_add(/* u64 */, /* u64 */) | ~~~~~~~~~~~~~~~~~~~~~~ error[E0308]: mismatched types --> src/main.rs:261:3 | 260 | fn CertiCoq_Benchmarks_lib_vs_add_id(&'a self) -> &'a dyn Fn(u64) -> &'a dyn Fn(u64) -> u6... | ----------------------------------------- expected `&'a (dyn Fn(u64) -> &'a (dyn Fn(u64) -> u64 + 'a) + 'a)` because of return type 261 | self.Coq_PArith_BinPosDef_Pos_add() | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `&dyn Fn(u64) -> &...`, found `u64` | = note: expected reference `&'a (dyn Fn(u64) -> &'a (dyn Fn(u64) -> u64 + 'a) + 'a)` found type `u64` error[E0061]: this method takes 2 arguments but 0 arguments were supplied --> src/main.rs:302:12 | 302 | self.Coq_PArith_BinPosDef_Pos_add()( | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing | note: method defined here --> src/main.rs:258:4 | 258 | fn Coq_PArith_BinPosDef_Pos_add(&'a self, a: u64, b: u64) -> u64 { a + b } | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------ ------ help: provide the arguments | 302 | self.Coq_PArith_BinPosDef_Pos_add(/* u64 */, /* u64 */)( | ~~~~~~~~~~~~~~~~~~~~~~ error[E0618]: expected function, found `u64` --> src/main.rs:302:7 | 302 | self.Coq_PArith_BinPosDef_Pos_add()( | -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;` | _______| | | 303 | | p)( | |__________- call expression requires function error[E0061]: this method takes 2 arguments but 0 arguments were supplied --> src/main.rs:509:16 | 509 | self.Coq_PArith_BinPosDef_Pos_compare()( | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing | note: method defined here --> src/main.rs:383:4 | 383 | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::O... | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------ ------ help: provide the arguments | 509 | self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)( | ~~~~~~~~~~~~~~~~~~~~~~ error[E0618]: expected function, found `std::cmp::Ordering` --> src/main.rs:509:11 | 509 | self.Coq_PArith_BinPosDef_Pos_compare()( | -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;` | ___________| | | 510 | | v)( | |______________- call expression requires function error[E0061]: this method takes 2 arguments but 0 arguments were supplied --> src/main.rs:784:14 | 784 | match self.Coq_PArith_BinPosDef_Pos_compare()( | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing | note: method defined here --> src/main.rs:383:4 | 383 | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::O... | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------ ------ help: provide the arguments | 784 | match self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)( | ~~~~~~~~~~~~~~~~~~~~~~ error[E0618]: expected function, found `std::cmp::Ordering` --> src/main.rs:784:9 | 784 | match self.Coq_PArith_BinPosDef_Pos_compare()( | -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;` | _________| | | 785 | | self.CertiCoq_Benchmarks_lib_vs_clause_prio( 786 | | cl1))( | |_________________- call expression requires function error[E0061]: this method takes 2 arguments but 0 arguments were supplied --> src/main.rs:2689:18 | 2689 | match self.Coq_PArith_BinPosDef_Pos_compare()( | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing | note: method defined here --> src/main.rs:383:4 | 383 | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::... | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------ ------ help: provide the arguments | 2689 | match self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)( | ~~~~~~~~~~~~~~~~~~~~~~ error[E0618]: expected function, found `std::cmp::Ordering` --> src/main.rs:2689:13 | 2689 | match self.Coq_PArith_BinPosDef_Pos_compare()( | -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;` | _____________| | | 2690 | | i)( | |________________- call expression requires function error[E0308]: mismatched types --> src/main.rs:3765:29 | 3762 | self.CertiCoq_Benchmarks_lib_vs_mergeC( | --------------------------------- arguments to this method are incorrect ... 3765 | / self.Coq_Init_Datatypes_id()( 3766 | | ()), | |_________________________________^ expected `&dyn Fn(&...) -> ...`, found `&dyn Fn(())` | = note: expected reference `&dyn Fn(&CertiCoq_Benchmarks_lib_vs_expr<'_>) -> &CertiCoq_Benchmarks_lib_vs_expr<'_>` found reference `&dyn Fn(())` note: method defined here --> src/main.rs:3658:4 | 3658 | fn CertiCoq_Benchmarks_lib_vs_mergeC(&'a self, A_cmp: &'a dyn Fn(A) -> &'a dyn Fn(A) -> std::cmp::Ordering, B_cmp: &'a dyn Fn(B) -> &'a dyn Fn(B) -> std::cmp::Ordering, fAB: &'a dyn Fn(A) -> B, a... | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ----------------------- error[E0061]: this method takes 2 arguments but 0 arguments were supplied --> src/main.rs:6533:10 | 6533 | self.Coq_PArith_BinPosDef_Pos_compare()( | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing | note: method defined here --> src/main.rs:383:4 | 383 | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::... | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------ ------ help: provide the arguments | 6533 | self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)( | ~~~~~~~~~~~~~~~~~~~~~~ error[E0618]: expected function, found `std::cmp::Ordering` --> src/main.rs:6533:5 | 6533 | self.Coq_PArith_BinPosDef_Pos_compare()( | -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;` | _____| | | 6534 | | i)( | |________- call expression requires function Some errors have detailed explanations: E0061, E0308, E0618. For more information about an error, try `rustc --explain E0061`. error: could not compile `vs_hard` (bin "vs_hard") due to 13 previous errors ```

Sha fast

``` Compiling sha_fast v0.1.0 (/home/wolfgang/ProjectsUni/Compilerstep/certicoqwasm-rustextraction/benchmarks/rust/sha_fast-extracted) error[E0282]: type annotations needed --> src/main.rs:620:24 | 67 | let $p2 = n.unsigned_abs(); | - type must be known at this point ... 620 | self.closure(move |x0| { | ^^ | help: consider giving this closure parameter an explicit type | 620 | self.closure(move |x0: /* Type */| { | ++++++++++++ For more information about this error, try `rustc --explain E0282`. error: could not compile `sha_fast` (bin "sha_fast") due to 1 previous error ```

workingjubilee commented 7 months ago

minor comment:

Sha fast: It is not guaranteed that type inference will succeed or that the inference algorithm will remain unchanged. If the types are known to the code generator, the generated code should emit the type annotations at appropriate binding sites, like closure arguments. Even if this was not done in every place possible (and it should probably only be done in a few places), this would make the code more resilient to small changes in the inference algorithm.

spitters commented 7 months ago

Thanks @womeier ! Quick answer. It looks like the Coq code uses loop as a term, which is a keyword in rust. I believe there is some renaming going on in the rust extraction to catch this, but apparently not for "loop". One could either rename loop to loop42 in the extraction, or write an algorithm that makes sure one generates a fresh name.

spitters commented 7 months ago

Welcome @workingjubilee ! Thanks for your interest in the experimental (!) rust extraction. Have you tried it yourself on examples?

There is some type information available at extraction time, but it may not be complete. See sec 5.5 here https://arxiv.org/pdf/2108.02995.pdf

4ever2 commented 7 months ago

@spitters I believe that this exact issue with renaming the loop keyword was discussed before (cannot remember where) but I don't think we have any pre-processing step to rename keywords.

We definitely need some better tests for the rust extraction plugin.

The remaining issues with vs_easy and vs_hard looks to be related to remapping of the stdlib type positive.

workingjubilee commented 7 months ago

I believe there is some renaming going on in the rust extraction to catch this, but apparently not for "loop".

Prefixing some of these idents with r# should work, allowing the following code to compile:

fn main() {
    let r#loop = loop {

    };
}

This may be a more general solution.

workingjubilee commented 7 months ago

Welcome @workingjubilee ! Thanks for your interest in the experimental (!) rust extraction. Have you tried it yourself on examples?

Honestly, you have won my attention by managing to induce SIGSEGV in the Rust compiler! I will try to make the binom.v Rust extraction compile, but I recommend avoiding that pattern in the future.

There is some type information available at extraction time, but it may not be complete.

For some cases, partial type information can be annotated via turbofished type arguments with an underscore to indicate the absent part, where relevant, e.g.

let v = iter.collect::<Vec<_>>();

spitters commented 7 months ago

@womeier For rust extraction we have the following tests: Ack and even: https://github.com/AU-COBRA/coq-rust-extraction/blob/master/tests/theories/InternalFix.v W: https://github.com/AU-COBRA/coq-rust-extraction/blob/master/tests/theories/BernsteinYangTermination.v

I think they should be relevant as general benchmarks for certicoq.

womeier commented 7 months ago

@womeier For rust extraction we have the following tests: Ack and even: https://github.com/AU-COBRA/coq-rust-extraction/blob/master/tests/theories/InternalFix.v W: https://github.com/AU-COBRA/coq-rust-extraction/blob/master/tests/theories/BernsteinYangTermination.v

I think they should be relevant as general benchmarks for certicoq.

yes, we'll include them. thanks!

womeier commented 6 months ago

Quick update: we needed a few more small manual fixes

some i64 annotations when using ExtrRustUncheckedArith
removing the derive(Debug) at a few places
reduced the error for vs_easy: replaced loop with loop42, and extracted without the remapping of nats (this introduced the additional problems in the original error in the issue description)
(some more information on our general setup here)

vs easy

``` error[E0308]: mismatched types --> src/main.rs:4243:29 | 4240 | self.CertiCoq_Benchmarks_lib_vs_mergeC( | --------------------------------- arguments to this method are incorrect ... 4243 | / self.Coq_Init_Datatypes_id()( 4244 | | ()), | |_________________________________^ expected `&dyn Fn(&...) -> ...`, found `&dyn Fn(())` | = note: expected reference `&dyn Fn(&CertiCoq_Benchmarks_lib_vs_expr<'_>) -> &CertiCoq_Benchmarks_lib_vs_expr<'_>` found reference `&dyn Fn(())` note: method defined here --> src/main.rs:4136:4 | 4136 | fn CertiCoq_Benchmarks_lib_vs_mergeC(&'a self, A_cmp: &'a dyn Fn(A) -> &'a dyn Fn(A) -> &'a Coq_Init_Datatypes_comparison<'a>, B_cmp: &'a dyn Fn(B) -> &'a dyn Fn(B) -> &'a Coq_Init_Datatypes_comparison<'a>, fAB: &'a dyn Fn(A) -> B, a... | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ----------------------- For more information about this error, try `rustc --explain E0308`. error: could not compile `vs_easy` (lib) due to 1 previous error

AU-COBRA / coq-rust-extraction