Merge pull request #379 from AeneasVerif/son/options

Check that the Charon options are correct

Makefile

@@ -152,12 +152,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 some temporary files which are inserted by, for instance, Emacs
-INPUTS_LIST := $(filter-out %~,$(INPUTS_LIST))
-INPUTS_LIST := $(filter-out .%,$(INPUTS_LIST))
-INPUTS_LIST := $(filter-out #%,$(INPUTS_LIST))
+# Remove the committed output files, as well as the temporary files
+INPUTS_LIST := $(filter-out %.out %~ .% %#,$(INPUTS_LIST))
 # Remove the directory prefix, replace with `test-`
 INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST))
 

README.md

@@ -74,6 +74,10 @@ If you run `make`, you will generate a documentation accessible from [`doc.html`
 
 ## Usage
 
+You should first generate the serialized `.llbc` file by calling Charon from *inside*
+(similarly to cargo) the crate you want to translate. **Important:** you should call
+Charon with the `--hide-marker-traits` option: `charon --hide-marker-traits`.
+
 The Aeneas binary is in `bin`; you can run: `./bin/aeneas -backend {fstar|coq|lean|hol4} [OPTIONS] LLBC_FILE`,
 where `LLBC_FILE` is an .llbc file generated by Charon.
 

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-1172606b471b5d9913f95cfbf944d3b943736667
+e6033230aab5cbff5e3840473844e913b59062af

src/Main.ml

@@ -136,8 +136,8 @@ let () =
   let filenames = ref [] in
   let add_filename f = filenames := f :: !filenames in
   Arg.parse spec add_filename usage;
-  let fail () =
-    print_string usage;
+  let fail (print_doc : bool) =
+    if print_doc then print_string usage;
     exit 1
   in
 
@@ -149,7 +149,11 @@ let () =
 
   let fail_with_error (msg : string) =
     log#serror msg;
-    fail ()
+    fail true
+  in
+  let fail_with_error_no_doc (msg : string) =
+    log#serror msg;
+    fail false
   in
 
   let check_arg_implies (arg0 : bool) (name0 : string) (arg1 : bool)
@@ -160,7 +164,7 @@ let () =
     else (
       log#error "Invalid command-line arguments: the use of %s requires %s"
         name0 name1;
-      fail ())
+      fail true)
   in
 
   let check_arg_not (arg0 : bool) (name0 : string) (arg1 : bool)
@@ -172,12 +176,15 @@ let () =
       log#error
         "Invalid command-line arguments: the use of %s is incompatible with %s"
         name0 name1;
-      fail ())
+      fail true)
   in
 
   let check (cond : bool) (msg : string) =
     if not cond then fail_with_error msg
   in
+  let check_no_doc (cond : bool) (msg : string) =
+    if not cond then fail_with_error_no_doc msg
+  in
 
   let check_not (cond : bool) (msg : string) =
     if cond then fail_with_error msg
@@ -259,7 +266,7 @@ let () =
             (* We don't support fuel for the HOL4 backend *)
             if !use_fuel then (
               log#error "The HOL4 backend doesn't support the -use-fuel option";
-              fail ()))
+              fail true))
   in
 
   (* Retrieve and check the filename *)
@@ -269,10 +276,10 @@ let () =
         (* TODO: update the extension *)
         if not (Filename.check_suffix f ".llbc") then (
           print_string ("Unrecognized file extension: " ^ f ^ "\n");
-          fail ())
+          fail true)
         else if not (Sys.file_exists f) then (
           print_string ("File not found: " ^ f ^ "\n");
-          fail ())
+          fail true)
         else f
     | _ ->
         (* For now, we only process one file at a time *)
@@ -295,6 +302,12 @@ let () =
       log#linfo (lazy ("Imported: " ^ filename));
       log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"));
 
+      (* Check the Charon CLI options *)
+      check_no_doc m.options.hide_marker_traits
+        "Invalid option detected: the serialized crate was generated by Charon \
+         without the `--hide-marker-traits` option. Please regenerate the \
+         crate by calling Charon with this option.\n";
+
       (* We don't support mutually recursive definitions with decreases clauses in Lean *)
       if
         !opt_backend = Some Lean && !extract_decreases_clauses
@@ -308,7 +321,7 @@ let () =
           "The Lean backend doesn't support the use of \
            decreasing_by/termination_by clauses with mutually recursive \
            definitions";
-        fail ());
+        fail true);
 
       (* There may be exceptions to catch *)
       (try

tests/src/mutually-recursive-traits.lean.out

@@ -13,4 +13,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 879, characters 2-52
 Called from Aeneas__Translate.extract_file in file "Translate.ml", line 1006, characters 2-36
 Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1576, characters 5-42
-Called from Dune__exe__Main in file "Main.ml", line 323, characters 14-66
+Called from Dune__exe__Main in file "Main.ml", line 336, characters 14-66