Merge branch 'main' into unsigned-max

4 files changed, 233 insertions, 154 deletions

diff --git a/tests/test_runner/aeneas_test_runner.opam b/tests/test_runner/aeneas_test_runner.opam
index b57cc9f6..1539c521 100644
--- a/tests/test_runner/aeneas_test_runner.opam
+++ b/tests/test_runner/aeneas_test_runner.opam
@@ -7,7 +7,7 @@ homepage: "https://github.com/AeneasVerif/aeneas"
 bug-reports: "https://github.com/AeneasVerif/aeneas/issues"
 depends: [
   "ocaml"
-  "dune" {>= "3.12"}
+  "dune" {>= "3.7"}
   "odoc" {with-doc}
 ]
 build: [
diff --git a/tests/test_runner/dune b/tests/test_runner/dune
index 7caf661f..1c719532 100644
--- a/tests/test_runner/dune
+++ b/tests/test_runner/dune
@@ -1,4 +1,10 @@
 (executable
  (public_name test_runner)
- (libraries core_unix.sys_unix unix)
+ (libraries core_unix.sys_unix re str unix)
+ (preprocess
+  (pps ppx_deriving.show ppx_deriving.ord ppx_sexp_conv))
  (name run_test))
+
+(env
+ (dev
+  (flags :standard -warn-error -5@8-11-14-32-33-20-21-26-27-39)))
diff --git a/tests/test_runner/dune-project b/tests/test_runner/dune-project
index c614e923..dc352bd0 100644
--- a/tests/test_runner/dune-project
+++ b/tests/test_runner/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.12)
+(lang dune 3.7)
 
 (name aeneas_test_runner)
 
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 8aa6347c..5d77bf9e 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;
@@ -5,23 +17,46 @@ type runner_env = {
   llbc_dir : string;
 }
 
-(* The data for a specific test to run aeneas on *)
-type aeneas_test_case = {
-  name : string;
-  backend : string;
-  subdir : string;
-  extra_aeneas_options : string list;
-}
+module Backend = struct
+  type t = Coq | Lean | FStar | HOL4 [@@deriving ord, sexp]
 
-type input_kind = SingleFile | Crate
+  (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
+  let all = [ Coq; Lean; FStar ]
 
-(* The data for a specific test to generate llbc for *)
-type charon_test_case = {
-  kind : input_kind;
-  name : string;
-  path : string;
-  extra_charon_options : string list;
-}
+  let of_string = function
+    | "coq" -> Coq
+    | "lean" -> Lean
+    | "fstar" -> FStar
+    | "hol4" -> HOL4
+    | backend -> failwith ("Unknown backend: `" ^ backend ^ "`")
+
+  let to_string = function
+    | Coq -> "coq"
+    | Lean -> "lean"
+    | FStar -> "fstar"
+    | HOL4 -> "hol4"
+end
+
+module BackendMap = struct
+  include Map.Make (Backend)
+
+  (* Make a new map with one entry per backend, given by `f` *)
+  let make (f : Backend.t -> 'a) : 'a t =
+    List.fold_left
+      (fun map backend -> add backend (f backend) map)
+      empty Backend.all
+
+  (* Set this value for all the backends in `backends` *)
+  let add_each (backends : Backend.t list) (v : 'a) (map : 'a t) : 'a t =
+    List.fold_left (fun map backend -> add backend v map) map backends
+
+  (* Updates all the backends in `backends` with `f` *)
+  let update_each (backends : Backend.t list) (f : 'a -> 'a) (map : 'a t) : 'a t
+      =
+    List.fold_left
+      (fun map backend -> update backend (Option.map f) map)
+      map backends
+end
 
 let concat_path = List.fold_left Filename.concat ""
 
@@ -42,21 +77,165 @@ let run_command args =
   let _ = Unix.waitpid [] pid in
   ()
 
+(* File-specific options *)
+let aeneas_options_for_test backend test_name =
+  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 =
+  match test_name with
+  | "betree" ->
+      [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
+  | _ -> []
+
+(* 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;
+    actions : action BackendMap.t;
+    charon_options : string list;
+    aeneas_options : string list BackendMap.t;
+    subdirs : string BackendMap.t;
+  }
+
+  (* The default subdirectory in which to store the outputs. *)
+  let default_subdir backend test_name =
+    match backend with Backend.Lean -> "." | _ -> test_name
+
+  (* 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;
+       - `subdir=...: set the subdirectory in which to store the outputs.
+            Defaults to nothing for lean and to the test name for other backends;
+       - `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.
+  *)
+  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
+    let subdir = Core.String.chop_prefix comment ~prefix:"subdir=" in
+
+    if comment = "skip" then
+      { input with actions = BackendMap.add_each backends Skip input.actions }
+    else if comment = "known-failure" then
+      {
+        input with
+        actions = BackendMap.add_each backends KnownFailure input.actions;
+      }
+    else if Option.is_some charon_args then
+      let args = Option.get charon_args in
+      let args = String.split_on_char ' ' args in
+      if backends != Backend.all then
+        failwith "Cannot set per-backend charon-args"
+      else { 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 =
+          BackendMap.update_each backends add_args input.aeneas_options;
+      }
+    else if Option.is_some subdir then
+      let subdir = Option.get subdir in
+      { input with subdirs = BackendMap.add_each backends subdir input.subdirs }
+    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 name = Str.global_replace (Str.regexp "-") "_" name in
+    let kind =
+      if Sys_unix.is_file_exn path then SingleFile
+      else if Sys_unix.is_directory_exn path then Crate
+      else failwith ("`" ^ path ^ "` is not a file or a directory.")
+    in
+    let actions = BackendMap.make (fun _ -> Normal) in
+    let charon_options = charon_options_for_test name in
+    let subdirs =
+      BackendMap.make (fun backend -> default_subdir backend name)
+    in
+    let aeneas_options =
+      BackendMap.make (fun backend -> aeneas_options_for_test backend name)
+    in
+    let input =
+      { path; name; kind; actions; charon_options; subdirs; 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 *)
-let run_aeneas (env : runner_env) (case : aeneas_test_case) =
-  let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
-  let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
+let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
+  (* FIXME: remove this special case *)
+  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 subdir = BackendMap.find backend case.subdirs 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 args =
     [|
-      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend;
+      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str;
     |]
   in
-  let args = Array.append args (Array.of_list case.extra_aeneas_options) in
+  let args = Array.append args (Array.of_list aeneas_options) in
   (* Run Aeneas *)
   run_command args
 
 (* Run Charon on a specific input with the given options *)
-let run_charon (env : runner_env) (case : charon_test_case) =
+let run_charon (env : runner_env) (case : Input.t) =
   match case.kind with
   | SingleFile ->
       let args =
@@ -71,16 +250,14 @@ let run_charon (env : runner_env) (case : charon_test_case) =
           env.llbc_dir;
         |]
       in
-      let args = Array.append args (Array.of_list case.extra_charon_options) in
+      let args = Array.append args (Array.of_list case.charon_options) in
       (* Run Charon on the rust file *)
       run_command args
   | Crate -> (
       match Sys.getenv_opt "IN_CI" with
       | None ->
           let args = [| env.charon_path; "--dest"; env.llbc_dir |] in
-          let args =
-            Array.append args (Array.of_list case.extra_charon_options)
-          in
+          let args = Array.append args (Array.of_list case.charon_options) in
           (* Run Charon inside the crate *)
           let old_pwd = Unix.getcwd () in
           Unix.chdir case.path;
@@ -94,140 +271,36 @@ let run_charon (env : runner_env) (case : charon_test_case) =
             "Warn: IN_CI is set; we skip generating llbc files for whole crates"
       )
 
-(* File-specific options *)
-let aeneas_options_for_test backend test_name =
-  (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *)
-  let use_fuel =
-    match (backend, test_name) with
-    | ( "coq",
-        ( "arrays" | "betree_main" | "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_main" | "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_main" ->
-        [
-          "-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
-
-(* 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
-
-(* The subdirectory in which to store the outputs. *)
-(* This reproduces the file layout that was set by the old Makefile. FIXME: cleanup *)
-let test_subdir backend test_name =
-  match (backend, test_name) with
-  | "lean", "demo" -> "Demo"
-  | "lean", _ -> "."
-  | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name
-  | _, "betree_main" -> "betree"
-  | _, "hashmap_main" -> "hashmap_on_disk"
-  | "hol4", _ -> "misc-" ^ test_name
-  | ( _,
-      ( "bitwise" | "constants" | "external" | "loops" | "no_nested_borrows"
-      | "paper" | "polonius_list" ) ) ->
-      "misc"
-  | _ -> test_name
-
 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 ->
       let runner_env = { charon_path; aeneas_path; llbc_dir } in
-      let test_name = Filename.remove_extension (Filename.basename test_path) in
-
-      let charon_kind =
-        if Sys_unix.is_file_exn test_path then SingleFile
-        else if Sys_unix.is_directory_exn test_path then Crate
-        else failwith ("`" ^ test_path ^ "` is not a file or a directory.")
-      in
-      let extra_charon_options = charon_options_for_test test_name in
-      let charon_case =
+      let test_case = Input.build test_path in
+      let test_case =
         {
-          path = test_path;
-          name = test_name;
-          kind = charon_kind;
-          extra_charon_options;
+          test_case with
+          aeneas_options =
+            BackendMap.map (List.append aeneas_options) test_case.aeneas_options;
         }
       in
-      (* Generate the llbc file *)
-      run_charon runner_env charon_case;
-
-      (* FIXME: remove this special case *)
-      let test_name =
-        if test_name = "betree" then "betree_main" else test_name
+      let skip_all =
+        List.for_all
+          (fun backend ->
+            BackendMap.find backend test_case.actions = Input.Skip)
+          Backend.all
       in
-      (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
-      let backends = [ "coq"; "lean"; "fstar" ] in
-      List.iter
-        (fun backend ->
-          let subdir = test_subdir backend test_name in
-          let extra_aeneas_options =
-            List.append
-              (aeneas_options_for_test backend test_name)
-              aeneas_options
-          in
-          let aeneas_case =
-            { name = test_name; backend; subdir; extra_aeneas_options }
-          in
-          (* Process the llbc file for the current backend *)
-          run_aeneas runner_env aeneas_case)
-        backends
+      if skip_all then ()
+      else (
+        (* 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)
   | _ -> failwith "Incorrect options passed to test runner"