From aa8e74197687ecc6d8f925babc8ba3cd6c739990 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Tue, 18 Jun 2024 22:47:35 +0200 Subject: Support for renaming using the rename attribute in charon (#239) * support for renaming using the rename attribute in charon * support for global decl * add support for renaming field * applied suggested changes and began adding support for variant * finished support for renaming variant * applied suggested changes * add tests * fixed variant and field renaming * update charon-pin * update flake.lock * Update the charon pin * Fix an issue with renaming trait method implementations * Fix an issue with the renaming of trait implementations * Fix an issue when renaming enumerations * Update the Charon pin * Fix the F* tests * Fix an issue with the spans for the loops * Fix the tests * Update a comment * Use fuel in the coq tests * Generate the template decreases clauses by default --------- Co-authored-by: Escherichia Co-authored-by: Son Ho --- tests/src/arrays.rs | 2 +- tests/src/betree/aeneas-test-options | 2 +- tests/src/hashmap.rs | 2 +- tests/src/loops.rs | 2 +- tests/src/mutually-recursive-traits.lean.out | 2 +- tests/src/rename_attribute.rs | 75 ++++++++++++++++++++++++++++ tests/src/traits.rs | 2 +- 7 files changed, 81 insertions(+), 6 deletions(-) create mode 100644 tests/src/rename_attribute.rs (limited to 'tests/src') diff --git a/tests/src/arrays.rs b/tests/src/arrays.rs index ddad2ad3..3d5b0e81 100644 --- a/tests/src/arrays.rs +++ b/tests/src/arrays.rs @@ -1,5 +1,5 @@ //@ [coq] aeneas-args=-use-fuel -//@ [fstar] aeneas-args=-decreases-clauses -template-clauses +//@ [fstar] aeneas-args=-decreases-clauses //@ [fstar] aeneas-args=-split-files //! Exercise the translation of arrays, with features supported by Eurydice diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options index 5a1e4180..c59ada7a 100644 --- a/tests/src/betree/aeneas-test-options +++ b/tests/src/betree/aeneas-test-options @@ -1,4 +1,4 @@ charon-args=--polonius --opaque=betree_utils [!borrow-check] aeneas-args=-backward-no-state-update -test-trans-units -state -split-files [coq] aeneas-args=-use-fuel -[fstar] aeneas-args=-decreases-clauses -template-clauses +[fstar] aeneas-args=-decreases-clauses diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs index 9ff448db..12a95d0f 100644 --- a/tests/src/hashmap.rs +++ b/tests/src/hashmap.rs @@ -1,7 +1,7 @@ //@ charon-args=--opaque=utils //@ [!borrow-check] aeneas-args=-state -split-files //@ [coq] aeneas-args=-use-fuel -//@ [fstar] aeneas-args=-decreases-clauses -template-clauses +//@ [fstar] aeneas-args=-decreases-clauses //@ [lean] aeneas-args=-no-gen-lib-entry // ^ the `-no-gen-lib-entry` is because we add a custom import in the Hashmap.lean file: we do not // want to overwrite it. diff --git a/tests/src/loops.rs b/tests/src/loops.rs index afc52ace..8a558b9d 100644 --- a/tests/src/loops.rs +++ b/tests/src/loops.rs @@ -1,5 +1,5 @@ //@ [coq] aeneas-args=-use-fuel -//@ [fstar] aeneas-args=-decreases-clauses -template-clauses +//@ [fstar] aeneas-args=-decreases-clauses //@ [fstar] aeneas-args=-split-files //@ [coq,fstar] subdir=misc use std::vec::Vec; diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index d4ca5af3..dffbb470 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -14,4 +14,4 @@ Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52 Called from Aeneas__Translate.extract_file in file "Translate.ml", line 963, characters 2-36 Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1512, characters 5-42 -Called from Dune__exe__Main in file "Main.ml", line 314, characters 14-66 +Called from Dune__exe__Main in file "Main.ml", line 317, characters 14-66 diff --git a/tests/src/rename_attribute.rs b/tests/src/rename_attribute.rs new file mode 100644 index 00000000..78765817 --- /dev/null +++ b/tests/src/rename_attribute.rs @@ -0,0 +1,75 @@ +//@ [fstar] aeneas-args=-decreases-clauses -split-files +//@ [coq] aeneas-args=-use-fuel +#![feature(register_tool)] +#![register_tool(charon)] +#![register_tool(aeneas)] + +#[charon::rename("BoolTest")] +pub trait BoolTrait { + // Required method + #[charon::rename("getTest")] + fn get_bool(&self) -> bool; + + // Provided method + #[charon::rename("retTest")] + fn ret_true(&self) -> bool { + true + } +} + +#[charon::rename("BoolImpl")] +impl BoolTrait for bool { + fn get_bool(&self) -> bool { + *self + } +} + +#[charon::rename("BoolFn")] +pub fn test_bool_trait(x: bool) -> bool { + x.get_bool() && x.ret_true() +} + +#[charon::rename("TypeTest")] +type Test = i32; + +#[charon::rename("VariantsTest")] +enum SimpleEnum { + #[charon::rename("Variant1")] + FirstVariant, + SecondVariant, + ThirdVariant, +} + +#[charon::rename("StructTest")] +struct Foo { + #[charon::rename("FieldTest")] + field1: u32, +} + +#[charon::rename("Const_Test")] +const C: u32 = 100 + 10 + 1; + +#[aeneas::rename("Const_Aeneas11")] +const CA: u32 = 10 + 1; + +#[charon::rename("Factfn")] +fn factorial(n: u64) -> u64 { + if n <= 1 { + 1 + } else { + return n * factorial(n - 1); + } +} + +#[charon::rename("No_borrows_sum")] +pub fn sum(max: u32) -> u32 { + let mut i = 0; + let mut s = 0; + while i < max { + s += i; + i += 1; + } + + s *= 2; + s +} diff --git a/tests/src/traits.rs b/tests/src/traits.rs index fd50db8c..36389cdf 100644 --- a/tests/src/traits.rs +++ b/tests/src/traits.rs @@ -1,4 +1,4 @@ -//@ [fstar] aeneas-args=-decreases-clauses -template-clauses +//@ [fstar] aeneas-args=-decreases-clauses pub trait BoolTrait { // Required method fn get_bool(&self) -> bool; -- cgit v1.2.3