From 2b40c5c3de1ee2caca2c0072f812fea04b5a0238 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 14:59:10 +0200 Subject: tests: Merge the hashmap test files --- tests/src/hashmap.rs | 29 ++++++++++++++++++++++++++++- tests/src/hashmap_main.rs | 22 ---------------------- tests/src/hashmap_utils.rs | 13 ------------- 3 files changed, 28 insertions(+), 36 deletions(-) delete mode 100644 tests/src/hashmap_main.rs delete mode 100644 tests/src/hashmap_utils.rs (limited to 'tests/src') diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs index 4552e4f2..ccb96e1e 100644 --- a/tests/src/hashmap.rs +++ b/tests/src/hashmap.rs @@ -1,9 +1,11 @@ +//@ charon-args=--opaque=hashmap_utils +//@ aeneas-args=-state -split-files //@ [coq] aeneas-args=-use-fuel -//@ aeneas-args=-split-files //@ [fstar] aeneas-args=-decreases-clauses -template-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. +// Possible to add `--no-code-duplication` if we use the optimized MIR // TODO: reactivate -test-trans-units //! A hashmap implementation. @@ -314,6 +316,31 @@ impl HashMap { } } +// This is a module so we can tell charon to leave it opaque +mod hashmap_utils { + use crate::*; + + /// Serialize a hash map - we don't have traits, so we fix the type of the + /// values (this is not the interesting part anyway) + pub(crate) fn serialize(_hm: HashMap) { + unimplemented!(); + } + /// Deserialize a hash map - we don't have traits, so we fix the type of the + /// values (this is not the interesting part anyway) + pub(crate) fn deserialize() -> HashMap { + unimplemented!(); + } +} + +pub fn insert_on_disk(key: Key, value: u64) { + // Deserialize + let mut hm = hashmap_utils::deserialize(); + // Update + hm.insert(key, value); + // Serialize + hashmap_utils::serialize(hm); +} + /// I currently can't retrieve functions marked with the attribute #[test], /// while I want to extract the unit tests and use the normalize on them, /// so I have to define the test functions somewhere and call them from diff --git a/tests/src/hashmap_main.rs b/tests/src/hashmap_main.rs deleted file mode 100644 index 0c827844..00000000 --- a/tests/src/hashmap_main.rs +++ /dev/null @@ -1,22 +0,0 @@ -//@ charon-args=--opaque=hashmap_utils -//@ aeneas-args=-state -split-files -//@ [coq] aeneas-args=-use-fuel -//@ [fstar] aeneas-args=-decreases-clauses -template-clauses -// Possible to add `--no-code-duplication` if we use the optimized MIR -// TODO: reactivate -test-trans-units -mod hashmap; -mod hashmap_utils; - -use crate::hashmap::*; -use crate::hashmap_utils::*; - -pub fn insert_on_disk(key: Key, value: u64) { - // Deserialize - let mut hm = deserialize(); - // Update - hm.insert(key, value); - // Serialize - serialize(hm); -} - -pub fn main() {} diff --git a/tests/src/hashmap_utils.rs b/tests/src/hashmap_utils.rs deleted file mode 100644 index 33de49e1..00000000 --- a/tests/src/hashmap_utils.rs +++ /dev/null @@ -1,13 +0,0 @@ -//@ skip -use crate::hashmap::*; - -/// Serialize a hash map - we don't have traits, so we fix the type of the -/// values (this is not the interesting part anyway) -pub(crate) fn serialize(_hm: HashMap) { - unimplemented!(); -} -/// Deserialize a hash map - we don't have traits, so we fix the type of the -/// values (this is not the interesting part anyway) -pub(crate) fn deserialize() -> HashMap { - unimplemented!(); -} -- cgit v1.2.3 From 9cc69020773cc77965a6faa6f0d46f179de3d8b8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 17:22:07 +0200 Subject: runner: Store options for crate tests in a separate file --- tests/src/betree/aeneas-test-options | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 tests/src/betree/aeneas-test-options (limited to 'tests/src') diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options new file mode 100644 index 00000000..c71e01df --- /dev/null +++ b/tests/src/betree/aeneas-test-options @@ -0,0 +1,4 @@ +charon-args=--polonius --opaque=betree_utils +aeneas-args=-backward-no-state-update -test-trans-units -state -split-files +[coq] aeneas-args=-use-fuel +[fstar] aeneas-args=-decreases-clauses -template-clauses -- cgit v1.2.3 From c81c96f20b1dbf428a9ed42e83b910e798e1a225 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 17:33:56 +0200 Subject: Add some tests --- tests/src/infinite-loop.rs | 11 +++++++++++ tests/src/issue-194-recursive-struct-projector.rs | 16 ++++++++++++++++ tests/src/matches.rs | 10 ++++++++++ 3 files changed, 37 insertions(+) create mode 100644 tests/src/infinite-loop.rs create mode 100644 tests/src/issue-194-recursive-struct-projector.rs create mode 100644 tests/src/matches.rs (limited to 'tests/src') diff --git a/tests/src/infinite-loop.rs b/tests/src/infinite-loop.rs new file mode 100644 index 00000000..906fc1fa --- /dev/null +++ b/tests/src/infinite-loop.rs @@ -0,0 +1,11 @@ +//@ [coq,fstar,lean] skip +//@ [coq,fstar] aeneas-args=-use-fuel +//@ [coq,fstar] subdir=misc +// FIXME: make it work +fn bar() {} + +fn foo() { + loop { + bar() + } +} diff --git a/tests/src/issue-194-recursive-struct-projector.rs b/tests/src/issue-194-recursive-struct-projector.rs new file mode 100644 index 00000000..9ebdc2bc --- /dev/null +++ b/tests/src/issue-194-recursive-struct-projector.rs @@ -0,0 +1,16 @@ +//@ [coq,fstar] subdir=misc +struct AVLNode { + value: T, + left: AVLTree, + right: AVLTree, +} + +type AVLTree = Option>>; + +fn get_val(x: AVLNode) -> T { + x.value +} + +fn get_left(x: AVLNode) -> AVLTree { + x.left +} diff --git a/tests/src/matches.rs b/tests/src/matches.rs new file mode 100644 index 00000000..5710a604 --- /dev/null +++ b/tests/src/matches.rs @@ -0,0 +1,10 @@ +//@ [coq] skip +//@ [coq,fstar] subdir=misc +//^ note: coq gives "invalid notation for pattern" +fn match_u32(x: u32) -> u32 { + match x { + 0 => 0, + 1 => 1, + _ => 2, + } +} -- cgit v1.2.3 From c4d2af051c18c4c81b1e57a45210c37c89c8330f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 May 2024 11:18:35 +0200 Subject: tests: Rename hashmap_utils -> utils --- tests/src/hashmap.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'tests/src') diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs index ccb96e1e..19832a84 100644 --- a/tests/src/hashmap.rs +++ b/tests/src/hashmap.rs @@ -1,4 +1,4 @@ -//@ charon-args=--opaque=hashmap_utils +//@ charon-args=--opaque=utils //@ aeneas-args=-state -split-files //@ [coq] aeneas-args=-use-fuel //@ [fstar] aeneas-args=-decreases-clauses -template-clauses @@ -317,7 +317,7 @@ impl HashMap { } // This is a module so we can tell charon to leave it opaque -mod hashmap_utils { +mod utils { use crate::*; /// Serialize a hash map - we don't have traits, so we fix the type of the @@ -334,11 +334,11 @@ mod hashmap_utils { pub fn insert_on_disk(key: Key, value: u64) { // Deserialize - let mut hm = hashmap_utils::deserialize(); + let mut hm = utils::deserialize(); // Update hm.insert(key, value); // Serialize - hashmap_utils::serialize(hm); + utils::serialize(hm); } /// I currently can't retrieve functions marked with the attribute #[test], -- cgit v1.2.3