From c0a6916549b55fbae2226e4c34af45e500928645 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 May 2024 14:56:26 +0200 Subject: Fix running individual tests --- Makefile | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index b3dc9f2b..ca3bd66c 100644 --- a/Makefile +++ b/Makefile @@ -47,7 +47,12 @@ build-test-verify: build test verify # Build the project, without formatting the code .PHONY: build-dev +ifdef IN_CI +build-dev: + @true +else build-dev: build-bin build-lib build-bin-dir doc +endif .PHONY: build-bin build-bin: check-charon @@ -166,14 +171,13 @@ test-all: $(INPUTS_LIST) ifdef IN_CI # In CI we do extra sanity checks. test-%: AENEAS_OPTIONS += -checks -else -test-%: check-charon endif # Translate the given rust file to available backends. The test runner decides # which backends to use and sets test-specific options. +# Note: the tests have the fulle file name: `test-arrays.rs`, `test-loops.rs`, `test-betree`. .PHONY: test-% -test-%: +test-%: build-dev $(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(INPUTS_DIR)/"$*" $(AENEAS_OPTIONS) echo "# Test $* done" -- cgit v1.3.1 From 4d3778bea3112168645efc03308056ec341abb5f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 May 2024 15:47:20 +0200 Subject: runner: Pass options in special comments --- Makefile | 4 - tests/src/arrays.rs | 3 + tests/src/bitwise.rs | 1 + tests/src/constants.rs | 2 + tests/src/demo.rs | 1 + tests/src/external.rs | 3 + tests/src/hashmap.rs | 8 ++ tests/src/hashmap_main.rs | 6 ++ tests/src/hashmap_utils.rs | 1 + tests/src/loops.rs | 3 + tests/src/nested_borrows.rs | 2 + tests/src/no_nested_borrows.rs | 2 + tests/src/paper.rs | 2 + tests/src/polonius_list.rs | 2 + tests/src/traits.rs | 1 + tests/test_runner/dune | 2 +- tests/test_runner/run_test.ml | 189 ++++++++++++++++++++++++----------------- 17 files changed, 150 insertions(+), 82 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index ca3bd66c..bda88c74 100644 --- a/Makefile +++ b/Makefile @@ -159,10 +159,6 @@ verify: INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*) # Remove the directory prefix, replace with `test-` INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST)) -# Remove some tests we don't want to run. -# FIXME: move this information to the file itself -INPUTS_LIST := $(filter-out test-hashmap_utils.rs,$(INPUTS_LIST)) -INPUTS_LIST := $(filter-out test-nested_borrows.rs,$(INPUTS_LIST)) # Run all the tests we found. .PHONY: test-all diff --git a/tests/src/arrays.rs b/tests/src/arrays.rs index 1f094541..ddad2ad3 100644 --- a/tests/src/arrays.rs +++ b/tests/src/arrays.rs @@ -1,3 +1,6 @@ +//@ [coq] aeneas-args=-use-fuel +//@ [fstar] aeneas-args=-decreases-clauses -template-clauses +//@ [fstar] aeneas-args=-split-files //! Exercise the translation of arrays, with features supported by Eurydice pub enum AB { diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs index 9f48cb04..15962047 100644 --- a/tests/src/bitwise.rs +++ b/tests/src/bitwise.rs @@ -1,3 +1,4 @@ +//@ aeneas-args=-test-trans-units //! Exercise the bitwise operations pub fn shift_u32(a: u32) -> u32 { diff --git a/tests/src/constants.rs b/tests/src/constants.rs index 83904eed..925c62b1 100644 --- a/tests/src/constants.rs +++ b/tests/src/constants.rs @@ -1,3 +1,5 @@ +//@ charon-args=--no-code-duplication +//@ aeneas-args=-test-trans-units //! Tests with constants // Integers diff --git a/tests/src/demo.rs b/tests/src/demo.rs index bc74cc8b..b9bb7ca2 100644 --- a/tests/src/demo.rs +++ b/tests/src/demo.rs @@ -1,3 +1,4 @@ +//@ [coq,fstar] aeneas-args=-use-fuel #![allow(clippy::needless_lifetimes)] /* Simple functions */ diff --git a/tests/src/external.rs b/tests/src/external.rs index 521749d6..ddd5539f 100644 --- a/tests/src/external.rs +++ b/tests/src/external.rs @@ -1,3 +1,6 @@ +//@ charon-args=--no-code-duplication +//@ aeneas-args=-state -split-files +//@ aeneas-args=-test-trans-units //! This module uses external types and functions use std::cell::Cell; diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs index 58d22acd..4552e4f2 100644 --- a/tests/src/hashmap.rs +++ b/tests/src/hashmap.rs @@ -1,3 +1,11 @@ +//@ [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. +// TODO: reactivate -test-trans-units + //! A hashmap implementation. //! //! Current limitations: diff --git a/tests/src/hashmap_main.rs b/tests/src/hashmap_main.rs index 45dfa6e2..0c827844 100644 --- a/tests/src/hashmap_main.rs +++ b/tests/src/hashmap_main.rs @@ -1,3 +1,9 @@ +//@ 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; diff --git a/tests/src/hashmap_utils.rs b/tests/src/hashmap_utils.rs index cd7b481f..33de49e1 100644 --- a/tests/src/hashmap_utils.rs +++ b/tests/src/hashmap_utils.rs @@ -1,3 +1,4 @@ +//@ skip use crate::hashmap::*; /// Serialize a hash map - we don't have traits, so we fix the type of the diff --git a/tests/src/loops.rs b/tests/src/loops.rs index 2f71d75b..8692c60e 100644 --- a/tests/src/loops.rs +++ b/tests/src/loops.rs @@ -1,3 +1,6 @@ +//@ [coq] aeneas-args=-use-fuel +//@ [fstar] aeneas-args=-decreases-clauses -template-clauses +//@ [fstar] aeneas-args=-split-files use std::vec::Vec; /// No borrows diff --git a/tests/src/nested_borrows.rs b/tests/src/nested_borrows.rs index 94db0cec..d4d8cf73 100644 --- a/tests/src/nested_borrows.rs +++ b/tests/src/nested_borrows.rs @@ -1,3 +1,5 @@ +//@ skip +//@ charon-args=--no-code-duplication //! This module contains functions with nested borrows in their signatures. pub fn id_mut_mut<'a, 'b, T>(x: &'a mut &'b mut T) -> &'a mut &'b mut T { diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs index 9a7604e6..78163371 100644 --- a/tests/src/no_nested_borrows.rs +++ b/tests/src/no_nested_borrows.rs @@ -1,3 +1,5 @@ +//@ charon-args=--no-code-duplication +//@ aeneas-args=-test-trans-units //! This module doesn't contain **functions which use nested borrows in their //! signatures**, and doesn't contain functions with loops. diff --git a/tests/src/paper.rs b/tests/src/paper.rs index 156f13ab..07453098 100644 --- a/tests/src/paper.rs +++ b/tests/src/paper.rs @@ -1,3 +1,5 @@ +//@ charon-args=--no-code-duplication +//@ aeneas-args=-test-trans-units //! The examples from the ICFP submission, all in one place. // 2.1 diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs index 8c64110d..a8d51e40 100644 --- a/tests/src/polonius_list.rs +++ b/tests/src/polonius_list.rs @@ -1,3 +1,5 @@ +//@ charon-args=--polonius +//@ aeneas-args=-test-trans-units #![allow(dead_code)] pub enum List { diff --git a/tests/src/traits.rs b/tests/src/traits.rs index 27c90586..fd50db8c 100644 --- a/tests/src/traits.rs +++ b/tests/src/traits.rs @@ -1,3 +1,4 @@ +//@ [fstar] aeneas-args=-decreases-clauses -template-clauses pub trait BoolTrait { // Required method fn get_bool(&self) -> bool; diff --git a/tests/test_runner/dune b/tests/test_runner/dune index 65b0c5fe..e8b29d66 100644 --- a/tests/test_runner/dune +++ b/tests/test_runner/dune @@ -1,6 +1,6 @@ (executable (public_name test_runner) - (libraries core_unix.sys_unix unix) + (libraries core_unix.sys_unix re unix) (preprocess (pps ppx_deriving.show ppx_deriving.ord ppx_sexp_conv)) (name run_test)) diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index e168069b..25efbcfd 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -1,3 +1,15 @@ +(* Convenience functions *) +let map_while (f : 'a -> 'b option) (input : 'a list) : 'b list = + let _, result = + List.fold_left + (fun (continue, out) a -> + if continue then + match f a with None -> (false, out) | Some b -> (true, b :: out) + else (continue, out)) + (true, []) input + in + List.rev result + (* Paths to use for tests *) type runner_env = { charon_path : string; @@ -48,78 +60,30 @@ let run_command args = (* File-specific options *) let aeneas_options_for_test backend test_name = - let backend = Backend.to_string backend in - (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *) - let use_fuel = - match (backend, test_name) with - | ( "coq", - ("arrays" | "betree" | "demo" | "hashmap" | "hashmap_main" | "loops") ) - -> - true - | "fstar", "demo" -> true - | _ -> false - in - let options = if use_fuel then "-use-fuel" :: [] else [] in - - let decrease_template_clauses = - backend = "fstar" - && - match test_name with - | "arrays" | "betree" | "hashmap" | "hashmap_main" | "loops" | "traits" -> - true - | _ -> false - in - let options = - if decrease_template_clauses then - "-decreases-clauses" :: "-template-clauses" :: options - else options - in - - let extra_options = - match (backend, test_name) with - | _, "betree" -> - [ - "-backward-no-state-update"; - "-test-trans-units"; - "-state"; - "-split-files"; - ] - | _, "bitwise" -> [ "-test-trans-units" ] - | _, "constants" -> [ "-test-trans-units" ] - | _, "external" -> [ "-test-trans-units"; "-state"; "-split-files" ] - | _, "hashmap_main" -> [ "-state"; "-split-files" ] - | _, "no_nested_borrows" -> [ "-test-trans-units" ] - | _, "paper" -> [ "-test-trans-units" ] - | _, "polonius_list" -> [ "-test-trans-units" ] - | "fstar", "arrays" -> [ "-split-files" ] - | "fstar", "loops" -> [ "-split-files" ] - (* We add a custom import in the Hashmap.lean file: we do not want to overwrite it *) - | "lean", "hashmap" -> [ "-split-files"; "-no-gen-lib-entry" ] - | _, "hashmap" -> [ "-split-files" ] - | _ -> [] - in - let options = List.append extra_options options in - options + if test_name = "betree" then + let options = + [ + "-backward-no-state-update"; + "-test-trans-units"; + "-state"; + "-split-files"; + ] + in + let extra_options = + match backend with + | Backend.Coq -> [ "-use-fuel" ] + | Backend.FStar -> [ "-decreases-clauses"; "-template-clauses" ] + | _ -> [] + in + List.append extra_options options + else [] (* File-specific options *) let charon_options_for_test test_name = - (* Possible to add `--no-code-duplication` for `hashmap_main` if we use the optimized MIR *) - let no_code_dup = - match test_name with - | "constants" | "external" | "nested_borrows" | "no_nested_borrows" - | "paper" -> - [ "--no-code-duplication" ] - | _ -> [] - in - let extra_options = - match test_name with - | "betree" -> - [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ] - | "hashmap_main" -> [ "--opaque=hashmap_utils" ] - | "polonius_list" -> [ "--polonius" ] - | _ -> [] - in - List.append no_code_dup extra_options + match test_name with + | "betree" -> + [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ] + | _ -> [] (* The subdirectory in which to store the outputs. *) (* This reproduces the file layout that was set by the old Makefile. FIXME: cleanup *) @@ -141,16 +105,66 @@ let test_subdir backend test_name = (* The data for a specific test input *) module Input = struct type kind = SingleFile | Crate + type action = Normal | Skip | KnownFailure type t = { name : string; path : string; kind : kind; + action : action; charon_options : string list; aeneas_options : string list BackendMap.t; subdir : string BackendMap.t; } + (* Parse lines that start `//@`. Each of them modifies the options we use for the test. + Supported comments: + - `skip`: don't process the file; + - `known-failure`: TODO; + - `charon-args=...`: extra arguments to pass to charon; + - `aeneas-args=...`: extra arguments to pass to aeneas; + - `[backend,..]...`: where each `backend` is the name of a backend supported by + aeneas; this sets options for these backends only. Only supported for `aeneas-args`. + *) + let apply_special_comment comment input = + let comment = String.trim comment in + (* Parse the backends if any *) + let re = Re.compile (Re.Pcre.re "^\\[([a-zA-Z,]+)\\](.*)$") in + let comment, (backends : Backend.t list) = + match Re.exec_opt re comment with + | Some groups -> + let backends = Re.Group.get groups 1 in + let backends = String.split_on_char ',' backends in + let backends = List.map Backend.of_string backends in + let rest = Re.Group.get groups 2 in + (String.trim rest, backends) + | None -> (comment, Backend.all) + in + (* Parse the other options *) + let charon_args = Core.String.chop_prefix comment ~prefix:"charon-args=" in + let aeneas_args = Core.String.chop_prefix comment ~prefix:"aeneas-args=" in + + if comment = "skip" then { input with action = Skip } + else if comment = "known-failure" then { input with action = KnownFailure } + else if Option.is_some charon_args then + let args = Option.get charon_args in + let args = String.split_on_char ' ' args in + { input with charon_options = List.append input.charon_options args } + else if Option.is_some aeneas_args then + let args = Option.get aeneas_args in + let args = String.split_on_char ' ' args in + let add_args opts = List.append opts args in + { + input with + aeneas_options = + List.fold_left + (fun map backend -> + BackendMap.update backend (Option.map add_args) map) + input.aeneas_options backends; + } + else failwith ("Unrecognized special comment: `" ^ comment ^ "`") + + (* Given a path to a rust file or crate, gather the details and options about how to build the test. *) let build (path : string) : t = let name = Filename.remove_extension (Filename.basename path) in let kind = @@ -158,6 +172,7 @@ module Input = struct else if Sys_unix.is_directory_exn path then Crate else failwith ("`" ^ path ^ "` is not a file or a directory.") in + let action = Normal in let charon_options = charon_options_for_test name in let subdir = List.fold_left @@ -173,7 +188,23 @@ module Input = struct BackendMap.add backend opts map) BackendMap.empty Backend.all in - { path; name; kind; charon_options; subdir; aeneas_options } + let input = + { path; name; kind; action; charon_options; subdir; aeneas_options } + in + match kind with + | SingleFile -> + let file_lines = Core.In_channel.read_lines path in + (* Extract the special lines. Stop at the first non-special line. *) + let special_comments = + map_while + (fun line -> Core.String.chop_prefix line ~prefix:"//@") + file_lines + in + (* Apply the changes from the special lines to our input. *) + List.fold_left + (fun input comment -> apply_special_comment comment input) + input special_comments + | Crate -> input end (* Run Aeneas on a specific input with the given options *) @@ -235,7 +266,7 @@ let () = match Array.to_list Sys.argv with (* Ad-hoc argument passing for now. *) | _exe_path :: charon_path :: aeneas_path :: llbc_dir :: test_path - :: aeneas_options -> + :: aeneas_options -> ( let runner_env = { charon_path; aeneas_path; llbc_dir } in let test_case = Input.build test_path in let test_case = @@ -246,10 +277,14 @@ let () = } in - (* Generate the llbc file *) - run_charon runner_env test_case; - (* Process the llbc file for the each backend *) - List.iter - (fun backend -> run_aeneas runner_env test_case backend) - Backend.all + match test_case.action with + | Skip -> () + | Normal -> + (* Generate the llbc file *) + run_charon runner_env test_case; + (* Process the llbc file for the each backend *) + List.iter + (fun backend -> run_aeneas runner_env test_case backend) + Backend.all + | KnownFailure -> failwith "KnownFailure is unimplemented") | _ -> failwith "Incorrect options passed to test runner" -- cgit v1.3.1 From 9c09789c26dd8142b8a29b42e250a685aa983e58 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 11:22:37 +0200 Subject: runner: Support negative tests --- Makefile | 4 +- flake.nix | 12 +++-- tests/lean/misc/MutuallyRecursiveTraits.lean | 6 +++ tests/src/mutually-recursive-traits.lean.out | 17 +++++++ tests/src/mutually-recursive-traits.rs | 11 +++++ tests/src/string-chars.lean.out | 21 +++++++++ tests/src/string-chars.rs | 6 +++ tests/test_runner/dune | 2 +- tests/test_runner/run_test.ml | 70 ++++++++++++++++++++-------- 9 files changed, 123 insertions(+), 26 deletions(-) create mode 100644 tests/lean/misc/MutuallyRecursiveTraits.lean create mode 100644 tests/src/mutually-recursive-traits.lean.out create mode 100644 tests/src/mutually-recursive-traits.rs create mode 100644 tests/src/string-chars.lean.out create mode 100644 tests/src/string-chars.rs (limited to 'Makefile') diff --git a/Makefile b/Makefile index bda88c74..38da9f7e 100644 --- a/Makefile +++ b/Makefile @@ -25,7 +25,7 @@ CHARON_OPTIONS ?= # The directory thta contains the rust source files for tests. INPUTS_DIR ?= tests/src # The directory where to look for the .llbc files. -LLBC_DIR ?= $(PWD)/tests/llbc +LLBC_DIR ?= tests/llbc # In CI, we enforce formatting and activate the (expensive) sanity checks. IN_CI ?= @@ -157,6 +157,8 @@ verify: # List the files and directories in `INPUTS_DIR` INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*) +# Remove the committed output files +INPUTS_LIST := $(filter-out %.out,$(INPUTS_LIST)) # Remove the directory prefix, replace with `test-` INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST)) diff --git a/flake.nix b/flake.nix index 68378954..f1a2258a 100644 --- a/flake.nix +++ b/flake.nix @@ -118,17 +118,19 @@ export CHARON_EXE=${charon.packages.${system}.charon}/bin/charon export TEST_RUNNER_EXE=${test_runner}/bin/test_runner - mkdir llbc - export LLBC_DIR=llbc - # Copy over the llbc file we can't generate ourselves. - cp ${betree-llbc}/llbc/betree_main.llbc $LLBC_DIR - # Copy the tests cp -r tests tests-copy make clean-generated-aeneas + mkdir tests/llbc + export LLBC_DIR=tests/llbc + # Copy over the llbc file we can't generate ourselves. + cp ${betree-llbc}/llbc/betree_main.llbc $LLBC_DIR + # Run the tests with extra sanity checks enabled IN_CI=1 make test-all -j $NIX_BUILD_CORES + # Clean generated llbc files so we don't compare them. + rm -r tests/llbc # Check that there are no differences between the generated tests # and the original tests diff --git a/tests/lean/misc/MutuallyRecursiveTraits.lean b/tests/lean/misc/MutuallyRecursiveTraits.lean new file mode 100644 index 00000000..b0fcb9e9 --- /dev/null +++ b/tests/lean/misc/MutuallyRecursiveTraits.lean @@ -0,0 +1,6 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [mutually_recursive_traits] +import Base +open Primitives + +namespace mutually_recursive_traits diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out new file mode 100644 index 00000000..33206fe5 --- /dev/null +++ b/tests/src/mutually-recursive-traits.lean.out @@ -0,0 +1,17 @@ +[Info ] Imported: tests/llbc/mutually_recursive_traits.llbc +[Error] In file Translate.ml, line 813: +Mutually recursive trait declarations are not supported + +Uncaught exception: + + (Failure + "In file Translate.ml, line 813:\ + \nIn file Translate.ml, line 813:\ + \nMutually recursive trait declarations are not supported") + +Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76 +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 954, characters 2-36 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1502, characters 5-42 +Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61 diff --git a/tests/src/mutually-recursive-traits.rs b/tests/src/mutually-recursive-traits.rs new file mode 100644 index 00000000..351763b2 --- /dev/null +++ b/tests/src/mutually-recursive-traits.rs @@ -0,0 +1,11 @@ +//@ [lean] known-failure +//@ [coq,fstar] skip +//@ subdir=misc +pub trait Trait1 { + type T: Trait2; +} + +pub trait Trait2: Trait1 {} + +pub trait T1>: Sized {} +pub trait T2>: Sized {} diff --git a/tests/src/string-chars.lean.out b/tests/src/string-chars.lean.out new file mode 100644 index 00000000..0d28744f --- /dev/null +++ b/tests/src/string-chars.lean.out @@ -0,0 +1,21 @@ +[Info ] Imported: tests/llbc/string_chars.llbc +[Error] In file SymbolicToPure.ml, line 588: +ADTs containing borrows are not supported yet +Source: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20 + +Uncaught exception: + + (Failure + "In file SymbolicToPure.ml, line 588:\ + \nIn file SymbolicToPure.ml, line 588:\ + \nADTs containing borrows are not supported yet\ + \nSource: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20\ + \nSource: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20") + +Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76 +Called from Aeneas__SymbolicToPure.translate_type_decl in file "SymbolicToPure.ml", line 588, characters 2-113 +Called from Aeneas__SymbolicToPure.translate_type_decls.(fun) in file "SymbolicToPure.ml", line 3923, characters 15-42 +Called from Stdlib__List.filter_map.aux in file "list.ml", line 258, characters 14-17 +Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 229, characters 19-64 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 981, characters 4-33 +Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61 diff --git a/tests/src/string-chars.rs b/tests/src/string-chars.rs new file mode 100644 index 00000000..5ba9a2d6 --- /dev/null +++ b/tests/src/string-chars.rs @@ -0,0 +1,6 @@ +//@ [lean] known-failure +//@ [coq,fstar] skip +fn main() { + let s = "hello"; + let _chs: Vec = s.chars().collect(); +} diff --git a/tests/test_runner/dune b/tests/test_runner/dune index c38e009c..6bb3f7b2 100644 --- a/tests/test_runner/dune +++ b/tests/test_runner/dune @@ -1,6 +1,6 @@ (executable (public_name test_runner) - (libraries core_unix core_unix.sys_unix re str unix) + (libraries core_unix core_unix.filename_unix core_unix.sys_unix re str unix) (preprocess (pps ppx_deriving.show ppx_deriving.ord ppx_sexp_conv)) (name run_test)) diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index a5a89317..7a52b6f3 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -15,6 +15,7 @@ type runner_env = { charon_path : string; aeneas_path : string; llbc_dir : string; + dest_dir : string; } module Backend = struct @@ -61,10 +62,12 @@ end let concat_path = List.fold_left Filename.concat "" module Command = struct - type t = { args : string array } + type t = { args : string array; redirect_out : Unix.file_descr option } type status = Success | Failure - let make (args : string list) : t = { args = Array.of_list args } + let make (args : string list) : t = + { args = Array.of_list args; redirect_out = None } + let to_string (cmd : t) = Core.String.concat_array ~sep:" " cmd.args (* Run the command and returns its exit status. *) @@ -73,10 +76,8 @@ module Command = struct print_endline ("[test_runner] Running: " ^ command_str); (* Run the command *) - let pid = - Unix.create_process cmd.args.(0) cmd.args Unix.stdin Unix.stdout - Unix.stderr - in + let out = Option.value cmd.redirect_out ~default:Unix.stdout in + let pid = Unix.create_process cmd.args.(0) cmd.args Unix.stdin out out in let status = Core_unix.waitpid (Core.Pid.of_int pid) in match status with | Ok () -> Success @@ -89,6 +90,14 @@ module Command = struct match run cmd with | Success -> () | Failure -> failwith ("Command `" ^ to_string cmd ^ "` failed.") + + (* Run the command and aborts the program if the command succeeded. *) + let run_command_expecting_failure cmd = + match run cmd with + | Success -> + failwith + ("Command `" ^ to_string cmd ^ "` succeeded but was expected to fail.") + | Failure -> () end let aeneas_options_for_test backend test_name = @@ -232,18 +241,43 @@ end (* Run Aeneas on a specific input with the given options *) let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) = (* FIXME: remove this special case *) + let backend_str = Backend.to_string backend in let test_name = if case.name = "betree" then "betree_main" else case.name in let input_file = concat_path [ env.llbc_dir; test_name ] ^ ".llbc" in + let output_file = + Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out" + in let subdir = BackendMap.find backend case.subdirs in + let dest_dir = concat_path [ env.dest_dir; backend_str; subdir ] in let aeneas_options = BackendMap.find backend case.aeneas_options in - let backend_str = Backend.to_string backend in - let dest_dir = concat_path [ "tests"; backend_str; subdir ] in + let action = BackendMap.find backend case.actions in + + (* Build the command *) let args = [ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str ] in - let args = List.append args aeneas_options in + let abort_on_error = + match action with + | Skip | Normal -> [] + | KnownFailure -> [ "-abort-on-error" ] + in + let args = List.concat [ args; aeneas_options; abort_on_error ] in + let cmd = Command.make args in + (* Remove leftover files if they're not needed anymore *) + (match action with + | (Skip | Normal) when Sys.file_exists output_file -> Sys.remove output_file + | _ -> ()); (* Run Aeneas *) - Command.run_command_expecting_success (Command.make args) + match action with + | Skip -> () + | Normal -> Command.run_command_expecting_success cmd + | KnownFailure -> + let out = + Core_unix.openfile ~mode:[ O_CREAT; O_TRUNC; O_WRONLY ] output_file + in + let cmd = { cmd with redirect_out = Some out } in + Command.run_command_expecting_failure cmd; + Unix.close out (* Run Charon on a specific input with the given options *) let run_charon (env : runner_env) (case : Input.t) = @@ -267,7 +301,9 @@ let run_charon (env : runner_env) (case : Input.t) = | Crate -> ( match Sys.getenv_opt "IN_CI" with | None -> - let args = [ env.charon_path; "--dest"; env.llbc_dir ] in + let args = + [ env.charon_path; "--dest"; Filename_unix.realpath env.llbc_dir ] + in let args = List.append args case.charon_options in (* Run Charon inside the crate *) let old_pwd = Unix.getcwd () in @@ -287,7 +323,9 @@ let () = (* Ad-hoc argument passing for now. *) | _exe_path :: charon_path :: aeneas_path :: llbc_dir :: test_path :: aeneas_options -> - let runner_env = { charon_path; aeneas_path; llbc_dir } in + let runner_env = + { charon_path; aeneas_path; llbc_dir; dest_dir = "tests" } + in let test_case = Input.build test_path in let test_case = { @@ -307,11 +345,5 @@ let () = (* Generate the llbc file *) run_charon runner_env test_case; (* Process the llbc file for the each backend *) - List.iter - (fun backend -> - match BackendMap.find backend test_case.actions with - | Skip -> () - | Normal -> run_aeneas runner_env test_case backend - | KnownFailure -> failwith "KnownFailure is unimplemented") - Backend.all) + List.iter (run_aeneas runner_env test_case) Backend.all) | _ -> failwith "Incorrect options passed to test runner" -- cgit v1.3.1 From b5046454b47aba598a42d3d775d2ec54dc57c75a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 May 2024 16:05:56 +0200 Subject: ci: Check correctness of the charon pinned commit --- .github/workflows/ci.yml | 6 ++++++ Makefile | 2 +- flake.nix | 1 + scripts/ci-check-charon-pin.sh | 22 ++++++++++++++++++++++ scripts/update-charon-pin.sh | 2 +- 5 files changed, 31 insertions(+), 2 deletions(-) create mode 100755 scripts/ci-check-charon-pin.sh (limited to 'Makefile') diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 56769cae..5ee28837 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -54,3 +54,9 @@ jobs: - uses: actions/checkout@v4 - uses: cachix/install-nix-action@v26 - run: nix develop --command bash -c "cd tests/lean && make" + + check-charon-pin: + runs-on: [self-hosted, linux, nix] + steps: + - uses: actions/checkout@v4 + - run: nix develop --command ./scripts/ci-check-charon-pin.sh diff --git a/Makefile b/Makefile index 38da9f7e..b27fe0de 100644 --- a/Makefile +++ b/Makefile @@ -90,7 +90,7 @@ update-charon-pin: # Keep the commit revision in `./charon-pin` as well so that non-nix users can # know which commit to use. ./charon-pin: flake.lock - nix-shell -p jq --run './scripts/update-charon-pin.sh' >> ./charon-pin + ./scripts/update-charon-pin.sh >> ./charon-pin # Checks that `./charon` contains a clone of charon at the required commit. # Also checks that `./charon/bin/charon` exists. diff --git a/flake.nix b/flake.nix index 654c0006..3e8b88de 100644 --- a/flake.nix +++ b/flake.nix @@ -226,6 +226,7 @@ pkgs.ocamlPackages.ocamlformat pkgs.ocamlPackages.menhir pkgs.ocamlPackages.odoc + pkgs.jq ]; inputsFrom = [ diff --git a/scripts/ci-check-charon-pin.sh b/scripts/ci-check-charon-pin.sh new file mode 100755 index 00000000..4aacd96e --- /dev/null +++ b/scripts/ci-check-charon-pin.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Checks that the charon pin: +# - moves forward from the previous pin, to ensure we don't regress the charon version; +# - is merged into Charon. + +NEW_CHARON_PIN="$(cat flake.lock | jq -r .nodes.charon.locked.rev)" +OLD_CHARON_PIN="$(git show origin/main:flake.lock | jq -r .nodes.charon.locked.rev)" +echo "This PR updates the charon pin from $OLD_CHARON_PIN to $NEW_CHARON_PIN" + +git clone https://github.com/AeneasVerif/charon +cd charon +CHARON_MAIN="$(git rev-parse HEAD)" + +if ! git merge-base --is-ancestor "$OLD_CHARON_PIN" "$NEW_CHARON_PIN"; then + echo "Error: the new charon pin does not have the old one as its ancestor. The pin must only move forward." + exit 1 +fi + +if ! git merge-base --is-ancestor "$NEW_CHARON_PIN" "$CHARON_MAIN"; then + echo "Error: commit $NEW_CHARON_PIN is not merged into Charon." + exit 1 +fi diff --git a/scripts/update-charon-pin.sh b/scripts/update-charon-pin.sh index 418602b8..63dfe3b6 100755 --- a/scripts/update-charon-pin.sh +++ b/scripts/update-charon-pin.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash if ! which jq 2> /dev/null 1>&2; then - echo 'Error: command `jq` not found.' + echo 'Error: command `jq` not found; please install it.' exit 1 fi echo '# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.' > ./charon-pin -- cgit v1.3.1 From 4195b9653b2d00b846edd3b74211f129192a8806 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 May 2024 15:36:08 +0200 Subject: Update charon pin to local commit when developing --- Makefile | 11 +++-------- scripts/update-charon-pin.sh | 11 +++++++++++ 2 files changed, 14 insertions(+), 8 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index b27fe0de..1e832378 100644 --- a/Makefile +++ b/Makefile @@ -81,16 +81,11 @@ build-bin-dir: build-bin build-lib build-runner doc: cd compiler && dune build @doc -# Fetches the latest commit from charon and updates `flake.lock` accordingly. +# Updates `flake.lock` and `charon-pin` with the latest commit from Charon. If +# we're using a symlink, this takes the commit from our local charon. .PHONY: update-charon-pin update-charon-pin: - nix flake lock --update-input charon - $(MAKE) charon-pin - -# Keep the commit revision in `./charon-pin` as well so that non-nix users can -# know which commit to use. -./charon-pin: flake.lock - ./scripts/update-charon-pin.sh >> ./charon-pin + ./scripts/update-charon-pin.sh # Checks that `./charon` contains a clone of charon at the required commit. # Also checks that `./charon/bin/charon` exists. diff --git a/scripts/update-charon-pin.sh b/scripts/update-charon-pin.sh index 63dfe3b6..1fa706ae 100755 --- a/scripts/update-charon-pin.sh +++ b/scripts/update-charon-pin.sh @@ -3,5 +3,16 @@ if ! which jq 2> /dev/null 1>&2; then echo 'Error: command `jq` not found; please install it.' exit 1 fi + +if [ -L charon ]; then + echo '`./charon` is a symlink; we using the commit there for our new pin.' + COMMIT="$(git -C charon rev-parse HEAD)" + nix flake lock --override-input charon "github:aeneasverif/charon/$COMMIT" +else + echo 'Pinning the latest commit from Charon `main`' + nix flake lock --update-input charon +fi + +# Keep the commit revision in `./charon-pin` as well so that non-nix users can know which commit to use. echo '# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.' > ./charon-pin jq -r .nodes.charon.locked.rev flake.lock >> ./charon-pin -- cgit v1.3.1