diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/BorrowCheck.ml | 28 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 18 | ||||
| -rw-r--r-- | compiler/Logging.ml | 3 | ||||
| -rw-r--r-- | compiler/Main.ml | 9 | ||||
| -rw-r--r-- | compiler/Translate.ml | 5 | ||||
| -rw-r--r-- | compiler/dune | 1 |
6 files changed, 54 insertions, 10 deletions
diff --git a/compiler/BorrowCheck.ml b/compiler/BorrowCheck.ml new file mode 100644 index 00000000..52f42c37 --- /dev/null +++ b/compiler/BorrowCheck.ml @@ -0,0 +1,28 @@ +open Interpreter +open LlbcAst + +(** The local logger *) +let log = Logging.borrow_check_log + +(** Borrow-check a crate. + + Note that we don't return anything: if we find borrow-checking errors, + we register them and print them later. + *) +let borrow_check_crate (crate : crate) : unit = + (* Debug *) + log#ldebug (lazy "translate_crate_to_pure"); + + (* Compute the translation context *) + let trans_ctx = compute_contexts crate in + + (* Borrow-check *) + let borrow_check_fun (fdef : fun_decl) : unit = + match fdef.body with + | None -> () + | Some _ -> + let synthesize = false in + let _ = evaluate_function_symbolic synthesize trans_ctx fdef in + () + in + List.iter borrow_check_fun (FunDeclId.Map.values crate.fun_decls) diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index fb3701f3..81d6ff72 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -489,9 +489,13 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) - the list of symbolic values introduced for the input values (this is useful for the synthesis) - the symbolic AST generated by the symbolic execution + + If [synthesize] is [true]: we synthesize the symbolic AST that is used for + the translation. Otherwise, we do not (the symbolic execution then simply + borrow-checks the function). *) -let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) : - symbolic_value list * SA.expression = +let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) + (fdef : fun_decl) : symbolic_value list * SA.expression option = (* Debug *) let name_to_string () = Print.Types.name_to_string @@ -615,9 +619,13 @@ let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) : let ctx_resl, cc = eval_function_body config (Option.get fdef.body).body ctx in - let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in - cc el - with CFailure (span, msg) -> Error (span, msg) + if synthesize then + (* Finish synthesizing *) + let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in + Some (cc el) + else None + with CFailure (span, msg) -> + if synthesize then Some (Error (span, msg)) else None in (* Return *) (input_svs, symbolic) diff --git a/compiler/Logging.ml b/compiler/Logging.ml index 9b8019b2..620c5fb5 100644 --- a/compiler/Logging.ml +++ b/compiler/Logging.ml @@ -15,6 +15,9 @@ let regions_hierarchy_log = L.get_logger "MainLogger.RegionsHierarchy" (** Logger for Translate *) let translate_log = L.get_logger "MainLogger.Translate" +(** Logger for BorrowCheck *) +let borrow_check_log = L.get_logger "MainLogger.BorrowCheck" + (** Logger for Contexts *) let contexts_log = L.get_logger "MainLogger.Contexts" diff --git a/compiler/Main.ml b/compiler/Main.ml index 557a3993..1bf9196a 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -309,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 @@ -323,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 diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 690bff5c..2bc9bb25 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -31,8 +31,9 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : | None -> None | Some _ -> (* Evaluate *) - let inputs, symb = evaluate_function_symbolic trans_ctx fdef in - Some (inputs, symb) + let synthesize = true in + let inputs, symb = evaluate_function_symbolic synthesize trans_ctx fdef in + Some (inputs, Option.get symb) (** Translate a function, by generating its forward and backward translations. diff --git a/compiler/dune b/compiler/dune index 6bdfd153..f987faec 100644 --- a/compiler/dune +++ b/compiler/dune @@ -14,6 +14,7 @@ (modules AssociatedTypes Assumed + BorrowCheck Collections Config ConstStrings |