summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.github/workflows/ci.yml6
-rw-r--r--Makefile107
-rw-r--r--README.md2
-rw-r--r--backends/lean/Base/Primitives/Base.lean5
-rw-r--r--compiler/ExtractTypes.ml3
-rw-r--r--compiler/InterpreterExpressions.ml12
-rw-r--r--compiler/Translate.ml5
-rw-r--r--flake.lock6
-rw-r--r--flake.nix3
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v2
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst2
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst2
-rw-r--r--tests/lean/Betree.lean1
-rw-r--r--tests/lean/BetreeMain/Funs.lean2
14 files changed, 62 insertions, 96 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 0ccc74e0..4826114e 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -1,7 +1,13 @@
on:
+ # Run the checks on any push to any branch of the repo that doesn't start with `_`.
push:
branches-ignore: [ '_**' ]
+ # Run the check for any pull request. The check is run on a merge between the
+ # PR commit and the `main` branch at the time of running the check.
pull_request:
+ # Runs the check when a PR is added to the merge queue.
+ merge_group:
+ # Makes it possible to run the forkflow by hand from GItHub's interface.
workflow_dispatch:
# Minimum permissions required by skip-duplicate-actions
diff --git a/Makefile b/Makefile
index 08359d49..414f562d 100644
--- a/Makefile
+++ b/Makefile
@@ -20,11 +20,6 @@ REGEN_LLBC ?=
# The path to Charon
CHARON_HOME ?= ../charon
-# The paths to the test directories in Charon (Aeneas will look for the .llbc
-# files in there).
-CHARON_TESTS_REGULAR_DIR ?= $(CHARON_HOME)/tests
-CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius
-
# The path to the Aeneas executable to run the tests - we need the ability to
# change this path for the Nix package.
AENEAS_EXE ?= bin/aeneas
@@ -36,7 +31,7 @@ OPTIONS ?=
# The rules use (and update) the following variables
#
# The Charon test directory where to look for the .llbc files
-CHARON_TEST_DIR =
+CHARON_TEST_DIR ?= $(CHARON_HOME)/tests
# The options with which to call Charon
CHARON_OPTIONS =
# The backend sub-directory in which to generate the files
@@ -94,8 +89,8 @@ test: build-dev test-all
test-all: test-no_nested_borrows test-paper \
test-hashmap test-hashmap_main \
test-external test-constants \
- testp-polonius_list testp-betree_main \
- ctest-testp-betree_main \
+ test-polonius_list test-betree_main \
+ ctest-test-betree_main \
test-loops \
test-arrays test-traits test-bitwise test-demo
@@ -183,14 +178,14 @@ tcoq-hashmap_main: OPTIONS += -use-fuel
tlean-hashmap_main: SUBDIR :=
thol4-hashmap_main: OPTIONS +=
-testp-polonius_list: OPTIONS += -test-trans-units
-testp-polonius_list: SUBDIR := misc
-tfstarp-polonius_list: OPTIONS +=
-tcoqp-polonius_list: OPTIONS +=
-tleanp-polonius_list: SUBDIR :=
-tleanp-polonius_list: OPTIONS +=
-thol4p-polonius_list: SUBDIR := misc-polonius_list
-thol4p-polonius_list: OPTIONS +=
+test-polonius_list: OPTIONS += -test-trans-units
+test-polonius_list: SUBDIR := misc
+tfstar-polonius_list: OPTIONS +=
+tcoq-polonius_list: OPTIONS +=
+tlean-polonius_list: SUBDIR :=
+tlean-polonius_list: OPTIONS +=
+thol4-polonius_list: SUBDIR := misc-polonius_list
+thol4-polonius_list: OPTIONS +=
test-constants: OPTIONS += -test-trans-units
test-constants: SUBDIR := misc
@@ -220,97 +215,57 @@ thol4-bitwise: SUBDIR := misc-bitwise
thol4-bitwise: OPTIONS +=
BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
-testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
-testp-betree_main: SUBDIR:=betree
-tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
-tcoqp-betree_main: OPTIONS += -use-fuel
-tleanp-betree_main: SUBDIR :=
-tleanp-betree_main: OPTIONS +=
+test-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
+test-betree_main: SUBDIR:=betree
+tfstar-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
+tcoq-betree_main: OPTIONS += -use-fuel
+tlean-betree_main: SUBDIR :=
+tlean-betree_main: OPTIONS +=
thol4-betree_main: OPTIONS +=
# Additional, *c*ustom test on the betree: translate it without `-backward-no-state-update`.
# This generates very ugly code, but is good to test the translation.
-.PHONY: ctest-testp-betree_main
-ctest-testp-betree_main: testp-betree_main
-ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units -state -split-files
-ctest-testp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
-ctest-testp-betree_main: BACKEND_SUBDIR := "fstar"
-ctest-testp-betree_main: SUBDIR:=betree_back_stateful
-ctest-testp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-ctest-testp-betree_main: FILE = betree_main
-ctest-testp-betree_main:
+.PHONY: ctest-test-betree_main
+ctest-test-betree_main: test-betree_main
+ctest-test-betree_main: OPTIONS += -backend fstar -test-trans-units -state -split-files
+ctest-test-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
+ctest-test-betree_main: BACKEND_SUBDIR := "fstar"
+ctest-test-betree_main: SUBDIR:=betree_back_stateful
+ctest-test-betree_main: FILE = betree_main
+ctest-test-betree_main:
$(AENEAS_CMD)
# Generic rules to extract the LLBC from a rust file
# We use the rules in Charon's Makefile to generate the .llbc files: the options
# vary with the test files.
.PHONY: gen-llbc-%
-gen-llbc-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
gen-llbc-%:
$(CHARON_CMD)
-# "p" stands for "Polonius"
-.PHONY: gen-llbcp-%
-gen-llbcp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-gen-llbcp-%:
- $(CHARON_CMD)
-
-# Generic rules to test the testlation of an LLBC file.
-# Note that the files requiring the Polonius borrow-checker are generated
-# in the tests-polonius subdirectory.
+# Generic rules to test the translation of an LLBC file.
.PHONY: test-%
-test-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
test-%: FILE = $*
test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-%
echo "# Test $* done"
-# "p" stands for "Polonius"
-.PHONY: testp-%
-testp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-testp-%: FILE = $*
-testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
- echo "# Test $* done"
-
.PHONY: tfstar-%
tfstar-%: OPTIONS += -backend fstar
tfstar-%: BACKEND_SUBDIR := fstar
tfstar-%:
$(AENEAS_CMD)
-# "p" stands for "Polonius"
-.PHONY: tfstarp-%
-tfstarp-%: OPTIONS += -backend fstar
-tfstarp-%: BACKEND_SUBDIR := fstar
-tfstarp-%:
- $(AENEAS_CMD)
-
.PHONY: tcoq-%
tcoq-%: OPTIONS += -backend coq
tcoq-%: BACKEND_SUBDIR := coq
tcoq-%:
$(AENEAS_CMD)
-# "p" stands for "Polonius"
-.PHONY: tcoqp-%
-tcoqp-%: OPTIONS += -backend coq
-tcoqp-%: BACKEND_SUBDIR := coq
-tcoqp-%:
- $(AENEAS_CMD)
-
.PHONY: tlean-%
tlean-%: OPTIONS += -backend lean
tlean-%: BACKEND_SUBDIR := lean
tlean-%:
$(AENEAS_CMD)
-# "p" stands for "Polonius"
-.PHONY: tleanp-%
-
-tleanp-%: OPTIONS += -backend lean
-tleanp-%: BACKEND_SUBDIR := lean
-tleanp-%:
- $(AENEAS_CMD)
-
# TODO: reactivate HOL4 once traits are parameterized by their associated types
.PHONY: thol4-%
thol4-%: OPTIONS += -backend hol4
@@ -321,16 +276,6 @@ thol4-%:
#thol4-%:
# $(AENEAS_CMD)
-# TODO: reactivate HOL4 once traits are parameterized by their associated types
-.PHONY: thol4p-%
-thol4p-%: OPTIONS += -backend hol4
-thol4p-%: BACKEND_SUBDIR := hol4
-thol4p-%:
- echo Ignoring the $* test for HOL4
-
-#thol4p-%:
-# $(AENEAS_CMD)
-
# Nix - TODO: add the lean tests
.PHONY: nix
nix:
diff --git a/README.md b/README.md
index 74de4500..3775ad9c 100644
--- a/README.md
+++ b/README.md
@@ -41,7 +41,7 @@ The dependencies can then be installed with the following command:
```
opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc \
- unionFind ocamlgraph
+ unionFind ocamlgraph menhir ocamlformat
```
Moreover, Aeneas requires the Charon ML library, defined in the
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index d682e926..c9237e65 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -134,7 +134,10 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ok x } :=
-- MISC --
----------
-@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : a × a := (x, x)
+-- This acts like a swap effectively in a functional pure world.
+-- We return the old value of `dst`, i.e. `dst` itself.
+-- The new value of `dst` is `src`.
+@[simp] def core.mem.replace (a : Type) (dst : a) (src : a) : a × a := (dst, src)
/- [core::option::Option::take] -/
@[simp] def Option.take (T: Type) (self: Option T): Option T × Option T := (self, .none)
/- [core::mem::swap] -/
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index c2eb8da0..947eceff 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -212,6 +212,9 @@ let extract_binop (meta : Meta.meta)
| Add -> "+"
| Sub -> "-"
| Mul -> "*"
+ | CheckedAdd | CheckedSub | CheckedMul ->
+ craise __FILE__ __LINE__ meta
+ "Checked operations are not implemented"
| Shl -> "<<<"
| Shr -> ">>>"
| BitXor -> "^^^"
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 5f849230..5a4fe7da 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -551,7 +551,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
| Ge -> Z.geq sv1.value sv2.value
| Gt -> Z.gt sv1.value sv2.value
| Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr | Shl
- | Shr | Ne | Eq ->
+ | Shr | Ne | Eq | CheckedAdd | CheckedSub | CheckedMul ->
craise __FILE__ __LINE__ meta "Unreachable"
in
Ok
@@ -575,7 +575,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
| BitXor -> raise Unimplemented
| BitAnd -> raise Unimplemented
| BitOr -> raise Unimplemented
- | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq ->
+ | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq | CheckedAdd
+ | CheckedSub | CheckedMul ->
craise __FILE__ __LINE__ meta "Unreachable"
in
match res with
@@ -586,7 +587,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
value = VLiteral (VScalar sv);
ty = TLiteral (TInteger sv1.int_ty);
})
- | Shl | Shr -> raise Unimplemented
+ | Shl | Shr | CheckedAdd | CheckedSub | CheckedMul ->
+ craise __FILE__ __LINE__ meta "Unimplemented binary operation"
| Ne | Eq -> craise __FILE__ __LINE__ meta "Unreachable")
| _ -> craise __FILE__ __LINE__ meta "Invalid inputs for binop"
@@ -633,6 +635,10 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
| Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr ->
sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta;
TLiteral (TInteger int_ty1)
+ (* These return `(int, bool)` which isn't a literal type *)
+ | CheckedAdd | CheckedSub | CheckedMul ->
+ craise __FILE__ __LINE__ meta
+ "Checked operations are not implemented"
| Shl | Shr ->
(* The number of bits can be of a different integer type
than the operand *)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 222b3c57..72a98c3d 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -798,7 +798,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
(* Translate *)
export_functions_group pure_funs
| GlobalGroup id -> export_global id
- | TraitDeclGroup id ->
+ | TraitDeclGroup (RecGroup _ids) ->
+ craise_opt_meta __FILE__ __LINE__ None
+ "Mutually recursive trait declarations are not supported"
+ | TraitDeclGroup (NonRecGroup id) ->
(* TODO: update to extract groups *)
if config.extract_trait_decls && config.extract_transparent then (
export_trait_decl_group id;
diff --git a/flake.lock b/flake.lock
index b3b55e6f..14ee3c05 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
"rust-overlay": "rust-overlay"
},
"locked": {
- "lastModified": 1714045526,
- "narHash": "sha256-ydEw01+8vnbGmgPXCXE22hJNRHUCJDnmU6yWlCvm2Ts=",
+ "lastModified": 1715003183,
+ "narHash": "sha256-/bnkg8txVHgM5X4t2j6TQmDQ22Rb3SCgCMV9pAQGjp8=",
"owner": "aeneasverif",
"repo": "charon",
- "rev": "04b69a9251046115325bd67264cbcb999b0e8048",
+ "rev": "1a205c55b02f3dff1ae238dfdac5a58d58de6006",
"type": "github"
},
"original": {
diff --git a/flake.nix b/flake.nix
index 6f868e3b..fd94d1d0 100644
--- a/flake.nix
+++ b/flake.nix
@@ -85,8 +85,7 @@
};
buildPhase = ''
# We need to provide the paths to the Charon tests derivations
- export CHARON_TESTS_REGULAR_DIR=${charon.checks.${system}.tests}
- export CHARON_TESTS_POLONIUS_DIR=${charon.checks.${system}.tests-polonius}
+ export CHARON_TEST_DIR=${charon.checks.${system}.tests}
# Copy the Aeneas executable, and update the path to it
cp ${aeneas}/bin/aeneas aeneas
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index c31713be..e0a1d8a2 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -827,7 +827,7 @@ Definition betree_BeTree_lookup
.
(** [betree_main::main]:
- Source: 'src/betree_main.rs', lines 5:0-5:9 *)
+ Source: 'src/main.rs', lines 4:0-4:9 *)
Definition main : result unit :=
Ok tt.
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 89396df0..9942ef68 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -667,7 +667,7 @@ let betree_BeTree_lookup
Ok (st1, (o, { self with root = n }))
(** [betree_main::main]:
- Source: 'src/betree_main.rs', lines 5:0-5:9 *)
+ Source: 'src/main.rs', lines 4:0-4:9 *)
let main : result unit =
Ok ()
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 89396df0..9942ef68 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -667,7 +667,7 @@ let betree_BeTree_lookup
Ok (st1, (o, { self with root = n }))
(** [betree_main::main]:
- Source: 'src/betree_main.rs', lines 5:0-5:9 *)
+ Source: 'src/main.rs', lines 4:0-4:9 *)
let main : result unit =
Ok ()
diff --git a/tests/lean/Betree.lean b/tests/lean/Betree.lean
new file mode 100644
index 00000000..58bee0c4
--- /dev/null
+++ b/tests/lean/Betree.lean
@@ -0,0 +1 @@
+import Betree.Funs
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index f0032d51..7cc52159 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -702,7 +702,7 @@ def betree.BeTree.lookup
Result.ok (st1, (o, { self with root := n }))
/- [betree_main::main]:
- Source: 'src/betree_main.rs', lines 5:0-5:9 -/
+ Source: 'src/main.rs', lines 4:0-4:9 -/
def main : Result Unit :=
Result.ok ()
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 12:54:24 +0000