diff options
author | Son HO | 2024-06-06 09:15:22 +0200 |
---|---|---|
committer | GitHub | 2024-06-06 09:15:22 +0200 |
commit | 961cc880311aed3319b08755c5a43816e2490d7f (patch) | |
tree | 80cc3d5db32d7198adbdf89e516484dc01e58186 /compiler/Main.ml | |
parent | baa0771885546816461e063131162b94c6954d86 (diff) | |
parent | a4dd9fe0598328976862868097f59207846d865c (diff) |
Merge pull request #233 from AeneasVerif/son/borrow-check
Add a `-borrow-check` option
Diffstat (limited to 'compiler/Main.ml')
-rw-r--r-- | compiler/Main.ml | 106 |
1 files changed, 73 insertions, 33 deletions
diff --git a/compiler/Main.ml b/compiler/Main.ml index 29322049..1bf9196a 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -68,9 +68,13 @@ let () = let spec_ls = [ + ( "-borrow-check", + Arg.Set borrow_check, + " Only borrow-check the program and do not generate any translation" ); ( "-backend", Arg.Symbol (backend_names, set_backend), - " Specify the target backend" ); + " Specify the target backend (" ^ String.concat ", " backend_names ^ ")" + ); ("-dest", Arg.Set_string dest_dir, " Specify the output directory"); ( "-test-units", Arg.Set test_unit_functions, @@ -137,6 +141,12 @@ let () = let check_arg_name name = assert (List.exists (fun (n, _, _) -> n = name) spec_ls) in + + let fail_with_error (msg : string) = + log#serror msg; + fail () + in + let check_arg_implies (arg0 : bool) (name0 : string) (arg1 : bool) (name1 : string) : unit = check_arg_name name0; @@ -160,6 +170,14 @@ let () = fail ()) in + let check (cond : bool) (msg : string) = + if not cond then fail_with_error msg + in + + let check_not (cond : bool) (msg : string) = + if cond then fail_with_error msg + in + if !print_llbc then main_log#set_level EL.Debug; (* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *) @@ -176,44 +194,63 @@ let () = check_arg_implies (not !generate_lib_entry_point) "-no-gen-lib-entry" !split_files "-split-files"; - if !lean_gen_lakefile && not (!backend = Lean) then - log#error + if !lean_gen_lakefile && not (backend () = Lean) then + fail_with_error "The -lean-default-lakefile option is valid only for the Lean backend"; + if !borrow_check then ( + check (!dest_dir = "") "Options -borrow-check and -dest are not compatible"; + check_not !split_files + "Options -borrow-check and -split-files are not compatible"; + check_not !test_unit_functions + "Options -borrow-check and -test-unit-functions are not compatible"; + check_not !test_trans_unit_functions + "Options -borrow-check and -test-trans-units are not compatible"; + check_not !extract_decreases_clauses + "Options -borrow-check and -decreases-clauses are not compatible"; + check_not !use_state + "Options -borrow-check and -use-state are not compatible"; + check_not !use_fuel "Options -borrow-check and -use-fuel are not compatible"; + check_not !split_files + "Options -borrow-check and -split-files are not compatible"); + (* Check that the user specified a backend *) let _ = match !opt_backend with - | Some b -> backend := b + | Some _ -> + check_not !borrow_check + "Arguments `-backend` and `-borrow-check` are not compatible" | None -> - log#error "Backend not specified (use the `-backend` argument)"; - fail () + check !borrow_check "Missing `-backend` or `-borrow-check` argument" in (* Set some options depending on the backend *) let _ = - match !backend with - | FStar -> - (* F* can disambiguate the field names *) - record_fields_short_names := true - | Coq -> - (* Some patterns are not supported *) - decompose_monadic_let_bindings := true; - decompose_nested_let_patterns := true - | Lean -> - (* We don't support fuel for the Lean backend *) - if !use_fuel then ( - log#error "The Lean backend doesn't support the -use-fuel option"; - fail ()); - (* Lean can disambiguate the field names *) - record_fields_short_names := true; - (* We exploit the fact that the variant name should always be - prefixed with the type name to prevent collisions *) - variant_concatenate_type_name := false - | HOL4 -> - (* 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 ()) + match !opt_backend with + | None -> () + | Some backend -> ( + match backend with + | FStar -> + (* F* can disambiguate the field names *) + record_fields_short_names := true + | Coq -> + (* Some patterns are not supported *) + decompose_monadic_let_bindings := true; + decompose_nested_let_patterns := true + | Lean -> + (* We don't support fuel for the Lean backend *) + check_not !use_fuel + "The Lean backend doesn't support the -use-fuel option"; + (* Lean can disambiguate the field names *) + record_fields_short_names := true; + (* We exploit the fact that the variant name should always be + prefixed with the type name to prevent collisions *) + variant_concatenate_type_name := false + | HOL4 -> + (* 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 ())) in (* Retrieve and check the filename *) @@ -251,7 +288,7 @@ let () = (* We don't support mutually recursive definitions with decreases clauses in Lean *) if - !backend = Lean && !extract_decreases_clauses + !opt_backend = Some Lean && !extract_decreases_clauses && List.exists (function | Aeneas.LlbcAst.FunGroup (RecGroup (_ :: _)) -> true @@ -272,8 +309,9 @@ let () = (* Test the unit functions with the concrete interpreter *) if !test_unit_functions then Test.test_unit_functions m; - (* Translate the functions *) - Aeneas.Translate.translate_crate filename dest_dir m + (* Translate or borrow-check the crate *) + if !borrow_check then Aeneas.BorrowCheck.borrow_check_crate m + else Aeneas.Translate.translate_crate filename dest_dir m with Errors.CFailure (_, _) -> (* In theory it shouldn't happen, but there may be uncaught errors - note that we let the [Failure] exceptions go through (they are @@ -286,7 +324,9 @@ let () = (* Reverse the list of error messages so that we print them from the earliest to the latest. *) (List.rev !Errors.error_list); - exit 1); + exit 1) + else if !borrow_check then + log#linfo (lazy "Crate successfully borrow-checked"); (* Print total elapsed time *) log#linfo |