From 35c6b1c3c3dbd1b782cb00206c773021f5c74765 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jun 2024 14:32:19 +0200 Subject: Add an option to run Aeneas as a borrow checker --- compiler/Config.ml | 22 ++++-- compiler/Extract.ml | 185 +++++++++++++++++++++++--------------------- compiler/ExtractBase.ml | 72 ++++++++--------- compiler/ExtractBuiltin.ml | 24 +++--- compiler/ExtractTypes.ml | 173 ++++++++++++++++++++++------------------- compiler/Main.ml | 97 ++++++++++++++++------- compiler/PureMicroPasses.ml | 4 +- compiler/PureUtils.ml | 2 +- compiler/SymbolicToPure.ml | 2 +- compiler/Translate.ml | 37 ++++----- 10 files changed, 342 insertions(+), 276 deletions(-) (limited to 'compiler') diff --git a/compiler/Config.ml b/compiler/Config.ml index 0b26e2ef..cb2c86ad 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -26,12 +26,22 @@ let set_backend (b : string) : unit = belonging to the proper set *) raise (Failure "Unexpected") -(** The backend to which to extract. +(** If [true], we do not generate code and simply borrow-check the program instead. + This allows us to relax some sanity checks which are present in the symbolic + execution only to make sure we will be able to generate the pure translation. + + Remark: when checking if we are borrow-checking a program, checking this + boolean or checking if [opt_backend] is [None] are equivalent. We need to + have different variables for the purpose of implementing the parsing of + the CI arguments. + *) +let borrow_check = ref false - We initialize it with a default value, but it always gets overwritten: - we check that the user provides a backend argument. - *) -let backend = ref FStar +(** Get the target backend *) +let backend () : backend = Option.get !opt_backend + +let if_backend (f : unit -> 'a) (default : 'a) : 'a = + match !opt_backend with None -> default | Some _ -> f () (** {1 Interpreter} *) @@ -361,7 +371,7 @@ let variant_concatenate_type_name = ref true let use_tuple_structs = ref true let backend_has_tuple_projectors () = - match !backend with Lean -> true | Coq | FStar | HOL4 -> false + match backend () with Lean -> true | Coq | FStar | HOL4 -> false (** We we use nested projectors for tuple (like: [(0, 1).snd.fst]) or do we use better projector syntax? *) diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 035ea8fe..eab85054 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -58,7 +58,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (* Add the termination measure *) let ctx = ctx_add_termination_measure def ctx in (* Add the decreases proof for Lean only *) - match !Config.backend with + match backend () with | Coq | FStar -> ctx | HOL4 -> craise __FILE__ __LINE__ def.span "Unexpected" | Lean -> ctx_add_decreases_proof def ctx @@ -98,7 +98,7 @@ let extract_adt_g_value (span : Meta.span) let extract_as_tuple () = (* This is very annoying: in Coq, we can't write [()] for the value of type [unit], we have to write [tt]. *) - if !backend = Coq && field_values = [] then ( + if backend () = Coq && field_values = [] then ( F.pp_print_string fmt "tt"; ctx) else @@ -108,7 +108,8 @@ let extract_adt_g_value (span : Meta.span) *) let lb, rb = if List.length field_values = 1 then ("", "") - else if !backend = Coq && is_single_pat && List.length field_values > 2 + else if + backend () = Coq && is_single_pat && List.length field_values > 2 then ("'(", ")") else ("(", ")") in @@ -150,7 +151,7 @@ let extract_adt_g_value (span : Meta.span) Otherwise, it is: `let Cons x0 ... xn = ...` *) - is_single_pat && !Config.backend = Lean + is_single_pat && backend () = Lean then ( F.pp_print_string fmt "⟨"; F.pp_print_space fmt (); @@ -273,7 +274,7 @@ let rec extract_typed_pattern (span : Meta.span) (ctx : extraction_ctx) block (because some of them are monadic) *) let lets_require_wrap_in_do (span : Meta.span) (lets : (bool * typed_pattern * texpression) list) : bool = - match !backend with + match backend () with | Lean -> (* For Lean, we wrap in a block iff at least one of the let-bindings is monadic *) List.exists (fun (m, _, _) -> m) lets @@ -299,7 +300,7 @@ let lets_require_wrap_in_do (span : Meta.span) *) let extract_texpression_errors (fmt : F.formatter) = - match !Config.backend with + match backend () with | FStar | Coq -> F.pp_print_string fmt "admit" | Lean -> F.pp_print_string fmt "sorry" | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)" @@ -360,7 +361,7 @@ and extract_App (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) const_name ctx in let add_brackets (s : string) = - if !backend = Coq then "(" ^ s ^ ")" else s + if backend () = Coq then "(" ^ s ^ ")" else s in F.pp_print_string fmt ("." ^ add_brackets name)) | _ -> @@ -472,7 +473,7 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx) method_name ctx in let add_brackets (s : string) = - if !backend = Coq then "(" ^ s ^ ")" else s + if backend () = Coq then "(" ^ s ^ ")" else s in F.pp_print_string fmt ("." ^ add_brackets fun_name)) else @@ -496,7 +497,7 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx) (* Sanity check: HOL4 doesn't support const generics *) sanity_check __FILE__ __LINE__ - (generics.const_generics = [] || !backend <> HOL4) + (generics.const_generics = [] || backend () <> HOL4) span; (* Print the generics. @@ -588,7 +589,7 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx) let field_name = (* Check if we need to extract the type as a tuple *) if is_tuple_struct then - match !backend with + match backend () with | FStar | HOL4 | Coq -> FieldId.to_string proj.field_id | Lean -> (* Tuples in Lean are syntax sugar for nested products/pairs, @@ -623,7 +624,7 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx) Note that the first "." is added below. *) let field_id = FieldId.to_int proj.field_id in - if !Config.use_nested_tuple_projectors then + if !use_nested_tuple_projectors then (* Nested projection: "2.2.2..." *) if field_id = 0 then "1" else @@ -640,10 +641,10 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx) (* Extract the expression *) extract_texpression span ctx fmt true arg; (* We allow to break where the "." appears (except Lean, it's a syntax error) *) - if !backend <> Lean then F.pp_print_break fmt 0 0; + if backend () <> Lean then F.pp_print_break fmt 0 0; F.pp_print_string fmt "."; (* If in Coq, the field projection has to be parenthesized *) - (match !backend with + (match backend () with | FStar | Lean | HOL4 -> F.pp_print_string fmt field_name | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")")); (* Close the box *) @@ -665,7 +666,7 @@ and extract_Lambda (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) (* Print the lambda - note that there should always be at least one variable *) sanity_check __FILE__ __LINE__ (xl <> []) span; F.pp_print_string fmt "fun"; - let with_type = !backend = Coq in + let with_type = backend () = Coq in let ctx = List.fold_left (fun ctx x -> @@ -674,7 +675,7 @@ and extract_Lambda (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) ctx xl in F.pp_print_space fmt (); - if !backend = Lean || !backend = Coq then F.pp_print_string fmt "=>" + if backend () = Lean || backend () = Coq then F.pp_print_string fmt "=>" else F.pp_print_string fmt "->"; F.pp_print_space fmt (); (* Print the body *) @@ -709,7 +710,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) ]} *) let lets, next_e = - match !backend with + match backend () with | HOL4 -> destruct_lets_no_interleave span e | FStar | Coq | Lean -> destruct_lets e in @@ -730,11 +731,11 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) * ]} * TODO: cleanup * *) - if monadic && (!backend = Coq || !backend = HOL4) then ( + if monadic && (backend () = Coq || backend () = HOL4) then ( let ctx = extract_typed_pattern span ctx fmt true true lv in F.pp_print_space fmt (); let arrow = - match !backend with + match backend () with | Coq | HOL4 -> "<-" | FStar | Lean -> craise __FILE__ __LINE__ span "impossible" in @@ -746,7 +747,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) else ( (* Print the "let" *) if monadic then - match !backend with + match backend () with | FStar -> F.pp_print_string fmt "let*"; F.pp_print_space fmt () @@ -760,7 +761,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) let ctx = extract_typed_pattern span ctx fmt true true lv in F.pp_print_space fmt (); let eq = - match !backend with + match backend () with | FStar -> "=" | Coq -> ":=" | Lean -> if monadic then "←" else ":=" @@ -770,7 +771,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); extract_texpression span ctx fmt false re; (* End the let-binding *) - (match !backend with + (match backend () with | Lean -> (* In Lean, (monadic) let-bindings don't require to end with anything *) () @@ -791,9 +792,9 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) at the end of every let-binding: let-bindings are indeed not ended with an "in" keyword. *) - if !Config.backend = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0; + if backend () = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0; (* Open parentheses *) - if inside && !backend <> Lean then F.pp_print_string fmt "("; + if inside && backend () <> Lean then F.pp_print_string fmt "("; (* If Lean and HOL4, we rely on monadic blocks, so we insert a do and open a new box immediately *) let wrap_in_do_od = lets_require_wrap_in_do span lets in @@ -814,11 +815,11 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) (* do-box (Lean and HOL4 only) *) if wrap_in_do_od then - if !backend = HOL4 then ( + if backend () = HOL4 then ( F.pp_print_space fmt (); F.pp_print_string fmt "od"); (* Close parentheses *) - if inside && !backend <> Lean then F.pp_print_string fmt ")"; + if inside && backend () <> Lean then F.pp_print_string fmt ")"; (* Close the box for the whole expression *) F.pp_close_box fmt () @@ -832,14 +833,14 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) In the case of Lean, we rely on indentation to delimit the end of the branches, and need to insert line breaks: we thus use a vbox. *) - if !Config.backend = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0; + if backend () = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0; (* Extract the switch *) (match body with | If (e_then, e_else) -> (* Open a box for the [if e] *) F.pp_open_hovbox fmt ctx.indent_incr; F.pp_print_string fmt "if"; - if !backend = Lean && ctx.use_dep_ite then F.pp_print_string fmt " h:"; + if backend () = Lean && ctx.use_dep_ite then F.pp_print_string fmt " h:"; F.pp_print_space fmt (); let scrut_inside = PureUtils.texpression_requires_parentheses span scrut @@ -863,7 +864,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) (* Open the parenthesized expression *) let print_space_after_parenth = if parenth then ( - match !backend with + match backend () with | FStar -> F.pp_print_space fmt (); F.pp_print_string fmt "begin"; @@ -885,7 +886,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) F.pp_close_box fmt (); (* Close the parenthesized expression *) (if parenth then - match !backend with + match backend () with | FStar -> F.pp_print_space fmt (); F.pp_print_string fmt "end" @@ -901,7 +902,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) F.pp_open_hovbox fmt ctx.indent_incr; (* Print the [match ... with] *) let match_begin = - match !backend with + match backend () with | FStar -> "begin match" | Coq -> "match" | Lean -> if ctx.use_dep_ite then "match h:" else "match" @@ -917,7 +918,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) extract_texpression span ctx fmt scrut_inside scrut; F.pp_print_space fmt (); let match_scrut_end = - match !backend with FStar | Coq | Lean -> "with" | HOL4 -> "of" + match backend () with FStar | Coq | Lean -> "with" | HOL4 -> "of" in F.pp_print_string fmt match_scrut_end; (* Close the box for the [match ... with] *) @@ -936,7 +937,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) let ctx = extract_typed_pattern span ctx fmt false false br.pat in F.pp_print_space fmt (); let arrow = - match !backend with FStar -> "->" | Coq | Lean | HOL4 -> "=>" + match backend () with FStar -> "->" | Coq | Lean | HOL4 -> "=>" in F.pp_print_string fmt arrow; (* Close the box for the pattern *) @@ -955,7 +956,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) List.iter extract_branch branches; (* End the match *) - match !backend with + match backend () with | Lean -> (*We rely on indentation in Lean *) () | FStar | Coq -> F.pp_print_space fmt (); @@ -969,11 +970,11 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx) unit = (* We can't update a subset of the fields in Coq (i.e., we can do [{| x:= 3; y := 4 |}], but there is no syntax for [{| s with x := 3 |}]) *) - sanity_check __FILE__ __LINE__ (!backend <> Coq || supd.init = None) span; + sanity_check __FILE__ __LINE__ (backend () <> Coq || supd.init = None) span; (* In the case of HOL4, records with no fields are not supported and are thus extracted to unit. We need to check that by looking up the definition *) let extract_as_unit = - match (!backend, supd.struct_id) with + match (backend (), supd.struct_id) with | HOL4, TAdtId adt_id -> let d = TypeDeclId.Map.find adt_id ctx.trans_ctx.type_ctx.type_decls in d.kind = Struct [] @@ -1009,14 +1010,14 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx) *) (* Outer brackets *) let olb, orb = - match !backend with + match backend () with | Lean | FStar -> (Some "{", Some "}") | Coq -> (Some "{|", Some "|}") | HOL4 -> (None, None) in (* Inner brackets *) let ilb, irb = - match !backend with + match backend () with | Lean | FStar | Coq -> (None, None) | HOL4 -> (Some "<|", Some "|>") in @@ -1030,7 +1031,7 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx) | None -> () in print_bracket true olb; - let need_paren = inside && !backend = HOL4 in + let need_paren = inside && backend () = HOL4 in if need_paren then F.pp_print_string fmt "("; F.pp_open_hvbox fmt ctx.indent_incr; if supd.init <> None then ( @@ -1042,10 +1043,10 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx) print_bracket true ilb; F.pp_open_hvbox fmt 0; let delimiter = - match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";" + match backend () with Lean -> "," | Coq | FStar | HOL4 -> ";" in let assign = - match !backend with Coq | Lean | HOL4 -> ":=" | FStar -> "=" + match backend () with Coq | Lean | HOL4 -> ":=" | FStar -> "=" in Collections.List.iter_link (fun () -> @@ -1093,7 +1094,7 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx) F.pp_close_box fmt (); (* Print the values *) let delimiter = - match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";" + match backend () with Lean -> "," | Coq | FStar | HOL4 -> ";" in F.pp_print_space fmt (); F.pp_open_hovbox fmt 0; @@ -1209,7 +1210,7 @@ let extract_fun_inputs_output_parameters_types (ctx : extraction_ctx) extract_ty def.span ctx fmt TypeDeclId.Set.empty false def.signature.output let assert_backend_supports_decreases_clauses (span : Meta.span) = - match !backend with + match backend () with | FStar | Lean -> () | _ -> craise __FILE__ __LINE__ span @@ -1233,7 +1234,9 @@ let assert_backend_supports_decreases_clauses (span : Meta.span) = *) let extract_template_fstar_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) (def : fun_decl) : unit = - cassert __FILE__ __LINE__ (!backend = FStar) def.span + cassert __FILE__ __LINE__ + (backend () = FStar) + def.span "The generation of template decrease clauses is only supported for the F* \ backend"; @@ -1245,7 +1248,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) (let name = - if !Config.extract_external_name_patterns && not def.is_local then + if !extract_external_name_patterns && not def.is_local then Some def.llbc_name else None in @@ -1302,7 +1305,9 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx) *) let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) (fmt : F.formatter) (def : fun_decl) : unit = - cassert __FILE__ __LINE__ (!backend = Lean) def.span + cassert __FILE__ __LINE__ + (backend () = Lean) + def.span "The generation of template termination and decreasing clauses is only \ supported for the Lean backend"; (* @@ -1414,7 +1419,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter) [ comment_pre ^ loop_comment ] in let name = - if !Config.extract_external_name_patterns && not def.is_local then + if !extract_external_name_patterns && not def.is_local then Some def.llbc_name else None in @@ -1433,7 +1438,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* Retrieve the function name *) let def_name = ctx_get_local_function def.span def.def_id def.loop_id ctx in (* Add a break before *) - if !backend <> HOL4 || not (decl_is_first_from_group kind) then + if backend () <> HOL4 || not (decl_is_first_from_group kind) then F.pp_print_break fmt 0 0; (* Print a comment to link the extracted definition to its original rust definition *) extract_fun_comment ctx fmt def; @@ -1443,7 +1448,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) F.pp_open_hvbox fmt 0; F.pp_open_vbox fmt ctx.indent_incr; (* For HOL4: we may need to put parentheses around the definition *) - let parenthesize = !backend = HOL4 && decl_is_not_last_from_group kind in + let parenthesize = backend () = HOL4 && decl_is_not_last_from_group kind in if parenthesize then F.pp_print_string fmt "("; (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *) F.pp_open_hovbox fmt ctx.indent_incr; @@ -1454,7 +1459,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) The boolean [is_opaque_coq] is used to detect this case. *) - let is_opaque_coq = !backend = Coq && is_opaque in + let is_opaque_coq = backend () = Coq && is_opaque in let use_forall = is_opaque_coq && def.signature.generics <> empty_generic_params in @@ -1502,7 +1507,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* [Tot] *) if has_decreases_clause then ( assert_backend_supports_decreases_clauses def.span; - if !backend = FStar then ( + if backend () = FStar then ( F.pp_print_string fmt "Tot"; F.pp_print_space fmt ())); extract_ty def.span ctx fmt TypeDeclId.Set.empty has_decreases_clause @@ -1511,7 +1516,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) F.pp_close_box fmt (); (* Print the decrease clause - rk.: a function with a decreases clause * is necessarily a transparent function *) - if has_decreases_clause && !backend = FStar then ( + if has_decreases_clause && backend () = FStar then ( assert_backend_supports_decreases_clauses def.span; F.pp_print_space fmt (); (* Open a box for the decreases clause *) @@ -1569,7 +1574,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* Print the "=" *) if not is_opaque then ( F.pp_print_space fmt (); - let eq = match !backend with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in + let eq = match backend () with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in F.pp_print_string fmt eq); (* Close the box for "(PARAMS) : EFFECT =" *) F.pp_close_box fmt (); @@ -1588,7 +1593,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* Close the inner box for the definition *) F.pp_close_box fmt (); (* Termination clause and proof for Lean *) - if has_decreases_clause && !backend = Lean then ( + if has_decreases_clause && backend () = Lean then ( let def_body = Option.get def.body in let all_vars = List.map (fun (v : var) -> v.id) def_body.inputs in let num_fwd_inputs = @@ -1659,10 +1664,10 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* Close the parentheses *) if parenthesize then F.pp_print_string fmt ")"; (* Add the definition end delimiter *) - if !backend = HOL4 && decl_is_not_last_from_group kind then ( + if backend () = HOL4 && decl_is_not_last_from_group kind then ( F.pp_print_space fmt (); F.pp_print_string fmt "/\\") - else if !backend = Coq && decl_is_last_from_group kind then ( + else if backend () = Coq && decl_is_last_from_group kind then ( (* This is actually an end of group delimiter. For aesthetic reasons we print it here instead of in {!end_fun_decl_group}. *) F.pp_print_cut fmt (); @@ -1670,7 +1675,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* Close the outer box for the definition *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) - if !backend <> HOL4 || decl_is_not_last_from_group kind then + if backend () <> HOL4 || decl_is_not_last_from_group kind then F.pp_print_break fmt 0 0 (** Extract an opaque function declaration to HOL4. @@ -1733,7 +1738,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit = sanity_check __FILE__ __LINE__ (not def.is_global_decl_body) def.span; (* We treat HOL4 opaque functions in a specific manner *) - if !backend = HOL4 && Option.is_none def.body then + if backend () = HOL4 && Option.is_none def.body then extract_fun_decl_hol4_opaque ctx fmt def else extract_fun_decl_gen ctx fmt kind has_decreases_clause def @@ -1752,7 +1757,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx) let is_opaque = Option.is_none extract_body in (* HOL4: Definition wrapper *) - if !backend = HOL4 then ( + if backend () = HOL4 then ( (* Open a vertical box: we *must* break lines *) F.pp_open_vbox fmt 0; F.pp_print_string fmt ("Definition " ^ name ^ "_def:"); @@ -1797,7 +1802,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx) if not is_opaque then ( (* Print " =" *) F.pp_print_space fmt (); - let eq = match !backend with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in + let eq = match backend () with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in F.pp_print_string fmt eq); (* Close ": TYPE =" box (depth=2) *) F.pp_close_box fmt (); @@ -1817,7 +1822,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx) F.pp_close_box fmt (); (* Coq: add a "." *) - if !backend = Coq then ( + if backend () = Coq then ( F.pp_print_cut fmt (); F.pp_print_string fmt "."); @@ -1825,7 +1830,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx) F.pp_close_box fmt (); (* HOL4: Definition wrapper *) - if !backend = HOL4 then ( + if backend () = HOL4 then ( F.pp_close_box fmt (); F.pp_print_space fmt (); F.pp_print_string fmt "End"; @@ -1888,7 +1893,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; let name = - if !Config.extract_external_name_patterns && not global.is_local then + if !extract_external_name_patterns && not global.is_local then Some global.llbc_name else None in @@ -1918,7 +1923,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter) | None -> (* No body: only generate a [val x_c : u32] declaration *) let kind = if interface then Declared else Assumed in - if !backend = HOL4 then + if backend () = HOL4 then extract_global_decl_hol4_opaque span ctx fmt decl_name global.generics decl_ty else @@ -1949,7 +1954,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter) let use_brackets = all_params <> [] in (* Extract the name *) let before, after = - match !backend with + match backend () with | FStar | Lean -> ( (fun () -> F.pp_print_string fmt "eval_global"; @@ -1994,7 +1999,7 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx) let name = ctx_compute_trait_parent_clause_name ctx trait_decl c in (* Add a prefix if necessary *) let name = - if !Config.record_fields_short_names then name + if !record_fields_short_names then name else ctx_compute_trait_decl_name ctx trait_decl ^ name in (c.clause_id, name)) @@ -2027,7 +2032,7 @@ let extract_trait_decl_register_constant_names (ctx : extraction_ctx) let name = ctx_compute_trait_const_name ctx trait_decl item_name in (* Add a prefix if necessary *) let name = - if !Config.record_fields_short_names then name + if !record_fields_short_names then name else ctx_compute_trait_decl_name ctx trait_decl ^ name in (item_name, name)) @@ -2061,7 +2066,7 @@ let extract_trait_decl_type_names (ctx : extraction_ctx) let type_name = ctx_compute_trait_type_name ctx trait_decl item_name in - if !Config.record_fields_short_names then type_name + if !record_fields_short_names then type_name else ctx_compute_trait_decl_name ctx trait_decl ^ type_name in let compute_clause_name (item_name : string) (clause : trait_clause) : @@ -2071,7 +2076,7 @@ let extract_trait_decl_type_names (ctx : extraction_ctx) in (* Add a prefix if necessary *) let name = - if !Config.record_fields_short_names then name + if !record_fields_short_names then name else ctx_compute_trait_decl_name ctx trait_decl ^ name in (clause.clause_id, name) @@ -2141,7 +2146,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx) let name = ctx_compute_fun_name f ctx in (* Add a prefix if necessary *) let name = - if !Config.record_fields_short_names then name + if !record_fields_short_names then name else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ name in (item_name, name) @@ -2271,7 +2276,7 @@ let extract_trait_item (ctx : extraction_ctx) (fmt : F.formatter) (* ":" or "=" *) F.pp_print_string fmt separator; ty (); - (match !Config.backend with Lean -> () | _ -> F.pp_print_string fmt ";"); + (match backend () with Lean -> () | _ -> F.pp_print_string fmt ";"); F.pp_close_box fmt () let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter) @@ -2280,7 +2285,7 @@ let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter) let extract_trait_impl_item (ctx : extraction_ctx) (fmt : F.formatter) (item_name : string) (ty : unit -> unit) : unit = - let assign = match !Config.backend with Lean | Coq -> ":=" | _ -> "=" in + let assign = match backend () with Lean | Coq -> ":=" | _ -> "=" in extract_trait_item ctx fmt item_name assign ty (** Small helper - TODO: move *) @@ -2325,7 +2330,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter) generics ctx in let backend_uses_forall = - match !backend with Coq | Lean -> true | FStar | HOL4 -> false + match backend () with Coq | Lean -> true | FStar | HOL4 -> false in let generics_not_empty = generics <> empty_generic_params in let use_forall = generics_not_empty && backend_uses_forall in @@ -2350,7 +2355,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) (let name = - if !Config.extract_external_name_patterns && not decl.is_local then + if !extract_external_name_patterns && not decl.is_local then Some decl.llbc_name else None in @@ -2364,7 +2369,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) There is just an exception with Lean: in this backend, line breaks are important for the parsing, so we always open a vertical box. *) - if !Config.backend = Lean then F.pp_open_vbox fmt ctx.indent_incr + if backend () = Lean then F.pp_open_vbox fmt ctx.indent_incr else ( F.pp_open_hvbox fmt 0; F.pp_open_hvbox fmt ctx.indent_incr); @@ -2378,7 +2383,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) (* When checking if the trait declaration is empty: we ignore the provided methods, because for now they are extracted separately *) let is_empty = trait_decl_is_empty { decl with provided_methods = [] } in - if !backend = FStar && not is_empty then ( + if backend () = FStar && not is_empty then ( F.pp_print_string fmt "noeq"; F.pp_print_space fmt ()); F.pp_print_string fmt qualif; @@ -2396,18 +2401,18 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) type_params cg_params trait_clauses; F.pp_print_space fmt (); - if is_empty && !backend = FStar then ( + if is_empty && backend () = FStar then ( F.pp_print_string fmt "= unit"; (* Outer box *) F.pp_close_box fmt ()) - else if is_empty && !backend = Coq then ( + else if is_empty && backend () = Coq then ( (* Coq is not very good at infering constructors *) let cons = ctx_get_trait_constructor decl.span decl.def_id ctx in F.pp_print_string fmt (":= " ^ cons ^ "{}."); (* Outer box *) F.pp_close_box fmt ()) else ( - (match !backend with + (match backend () with | Lean -> F.pp_print_string fmt "where" | FStar -> F.pp_print_string fmt "= {" | Coq -> @@ -2481,9 +2486,9 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) decl.required_methods; (* Close the outer boxes for the definition *) - if !Config.backend <> Lean then F.pp_close_box fmt (); + if backend () <> Lean then F.pp_close_box fmt (); (* Close the brackets *) - match !Config.backend with + match backend () with | Lean -> () | Coq -> F.pp_print_space fmt (); @@ -2554,7 +2559,7 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) (** See {!extract_trait_decl_coq_arguments} *) let extract_trait_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter) (trait_decl : trait_decl) : unit = - match !backend with + match backend () with | Coq -> extract_trait_decl_coq_arguments ctx fmt trait_decl | _ -> () @@ -2645,7 +2650,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) (let name, generics = - if !Config.extract_external_name_patterns && not impl.is_local then + if !extract_external_name_patterns && not impl.is_local then let decl_id = impl.impl_trait.trait_decl_id in let trait_decl = TraitDeclId.Map.find decl_id ctx.trans_trait_decls in let decl_ref = impl.llbc_impl_trait in @@ -2665,7 +2670,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) There is just an exception with Lean: in this backend, line breaks are important for the parsing, so we always open a vertical box. *) - if !Config.backend = Lean then ( + if backend () = Lean then ( F.pp_open_vbox fmt 0; F.pp_open_vbox fmt ctx.indent_incr) else ( @@ -2705,11 +2710,11 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) let is_empty = trait_impl_is_empty { impl with provided_methods = [] } in F.pp_print_space fmt (); - if is_empty && !Config.backend = FStar then ( + if is_empty && backend () = FStar then ( F.pp_print_string fmt "= ()"; (* Outer box *) F.pp_close_box fmt ()) - else if is_empty && !Config.backend = Coq then ( + else if is_empty && backend () = Coq then ( (* Coq is not very good at infering constructors *) let cons = ctx_get_trait_constructor impl.span impl.impl_trait.trait_decl_id ctx @@ -2718,8 +2723,8 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (* Outer box *) F.pp_close_box fmt ()) else ( - if !Config.backend = Lean then F.pp_print_string fmt ":= {" - else if !Config.backend = Coq then F.pp_print_string fmt ":= {|" + if backend () = Lean then F.pp_print_string fmt ":= {" + else if backend () = Coq then F.pp_print_string fmt ":= {|" else F.pp_print_string fmt "= {"; (* Close the box for the name + generics *) @@ -2811,10 +2816,10 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (* Close the outer boxes for the definition, as well as the brackets *) F.pp_close_box fmt (); - if !backend = Coq then ( + if backend () = Coq then ( F.pp_print_space fmt (); F.pp_print_string fmt "|}.") - else if (not (!backend = FStar)) || not is_empty then ( + else if (not (backend () = FStar)) || not is_empty then ( F.pp_print_space fmt (); F.pp_print_string fmt "}")); F.pp_close_box fmt (); @@ -2854,7 +2859,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) (* Open a box for the test *) F.pp_open_hovbox fmt ctx.indent_incr; (* Print the test *) - (match !backend with + (match backend () with | FStar -> F.pp_print_string fmt "let _ ="; F.pp_print_space fmt (); diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 815e228f..3346c328 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -495,14 +495,14 @@ let names_maps_add_function (id_to_string : id -> string) names_maps = names_maps_add id_to_string (FunId fid) span name nm -let bool_name () = if !backend = Lean then "Bool" else "bool" -let char_name () = if !backend = Lean then "Char" else "char" -let str_name () = if !backend = Lean then "String" else "string" +let bool_name () = if backend () = Lean then "Bool" else "bool" +let char_name () = if backend () = Lean then "Char" else "char" +let str_name () = if backend () = Lean then "String" else "string" (** Small helper to compute the name of an int type *) let int_name (int_ty : integer_type) : string = let isize, usize, i_format, u_format = - match !backend with + match backend () with | FStar | Coq | HOL4 -> ("isize", "usize", format_of_string "i%d", format_of_string "u%d") | Lean -> ("Isize", "Usize", format_of_string "I%d", format_of_string "U%d") @@ -525,9 +525,9 @@ let scalar_name (ty : literal_type) : string = match ty with | TInteger ty -> int_name ty | TBool -> ( - match !backend with FStar | Coq | HOL4 -> "bool" | Lean -> "Bool") + match backend () with FStar | Coq | HOL4 -> "bool" | Lean -> "Bool") | TChar -> ( - match !backend with FStar | Coq | HOL4 -> "char" | Lean -> "Char") + match backend () with FStar | Coq | HOL4 -> "char" | Lean -> "Char") (** Extraction context. @@ -786,13 +786,13 @@ let ctx_get_termination_measure (span : Meta.span) (def_id : A.FunDeclId.id) let unop_name (unop : unop) : string = match unop with | Not -> ( - match !backend with + match backend () with | FStar -> "not" | Lean -> "¬" | Coq -> "negb" | HOL4 -> "~") | Neg (int_ty : integer_type) -> ( - match !backend with Lean -> "-." | _ -> int_name int_ty ^ "_neg") + match backend () with Lean -> "-." | _ -> int_name int_ty ^ "_neg") | Cast _ -> (* We never directly use the unop name in this case *) raise (Failure "Unsupported") @@ -821,7 +821,7 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string = | _ -> raise (Failure "Unreachable") in (* Remark: the Lean case is actually not used *) - match !backend with + match backend () with | Lean -> int_name int_ty ^ "." ^ binop_s | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop_s @@ -843,7 +843,7 @@ let keywords () = named_binops in let misc = - match !backend with + match backend () with | FStar -> [ "assert"; @@ -1042,7 +1042,7 @@ let keywords () = let assumed_adts () : (assumed_ty * string) list = let state = if !use_state then - match !backend with + match backend () with | Lean -> [ (TState, "State") ] | Coq | FStar | HOL4 -> [ (TState, "state") ] else [] @@ -1051,7 +1051,7 @@ let assumed_adts () : (assumed_ty * string) list = referenced in the generated translation, and easily collides with user-defined types *) let adts = - match !backend with + match backend () with | Lean -> [ (TResult, "Result"); @@ -1065,7 +1065,7 @@ let assumed_adts () : (assumed_ty * string) list = | Coq | FStar | HOL4 -> [ (TResult, "result"); - (TFuel, if !backend = HOL4 then "num" else "nat"); + (TFuel, if backend () = HOL4 then "num" else "nat"); (TArray, "array"); (TSlice, "slice"); (TStr, "str"); @@ -1076,14 +1076,14 @@ let assumed_adts () : (assumed_ty * string) list = state @ adts let assumed_struct_constructors () : (assumed_ty * string) list = - match !backend with + match backend () with | Lean -> [ (TArray, "Array.make") ] | Coq -> [ (TArray, "mk_array") ] | FStar -> [ (TArray, "mk_array") ] | HOL4 -> [ (TArray, "mk_array") ] let assumed_variants () : (assumed_ty * VariantId.id * string) list = - match !backend with + match backend () with | FStar -> [ (TResult, result_ok_id, "Ok"); @@ -1123,7 +1123,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = ] let assumed_llbc_functions () : (A.assumed_fun_id * string) list = - match !backend with + match backend () with | FStar | Coq | HOL4 -> [ (ArrayIndexShared, "array_index_usize"); @@ -1146,7 +1146,7 @@ let assumed_llbc_functions () : (A.assumed_fun_id * string) list = ] let assumed_pure_functions () : (pure_assumed_fun_id * string) list = - match !backend with + match backend () with | FStar -> [ (Return, "return"); @@ -1258,7 +1258,7 @@ let initialize_names_maps () : names_maps = *) let type_decl_kind_to_qualif (span : Meta.span) (kind : decl_kind) (type_kind : type_decl_kind option) : string option = - match !backend with + match backend () with | FStar -> ( match kind with | SingleNonRec -> Some "type" @@ -1307,7 +1307,7 @@ let type_decl_kind_to_qualif (span : Meta.span) (kind : decl_kind) Remark: can return [None] for some backends like HOL4. *) let fun_decl_kind_to_qualif (kind : decl_kind) : string option = - match !backend with + match backend () with | FStar -> ( match kind with | SingleNonRec -> Some "let" @@ -1342,7 +1342,7 @@ let fun_decl_kind_to_qualif (kind : decl_kind) : string option = TODO: move inside the formatter? *) let type_keyword (span : Meta.span) = - match !backend with + match backend () with | FStar -> "Type0" | Coq | Lean -> "Type" | HOL4 -> craise __FILE__ __LINE__ span "Unexpected" @@ -1391,7 +1391,7 @@ let ctx_compute_type_name_no_suffix (span : Meta.span) (ctx : extraction_ctx) let ctx_compute_type_name (span : Meta.span) (ctx : extraction_ctx) (name : llbc_name) = let name = ctx_compute_type_name_no_suffix span ctx name in - match !backend with + match backend () with | FStar -> StringUtils.lowercase_first_letter (name ^ "_t") | Coq | HOL4 -> name ^ "_t" | Lean -> name @@ -1425,7 +1425,7 @@ let ctx_compute_field_name (span : Meta.span) (ctx : extraction_ctx) let def_name = ctx_compute_type_name_no_suffix span ctx def_name ^ "_" ^ field_name_s in - match !backend with + match backend () with | Lean | HOL4 -> def_name | Coq | FStar -> StringUtils.lowercase_first_letter def_name @@ -1435,7 +1435,7 @@ let ctx_compute_field_name (span : Meta.span) (ctx : extraction_ctx) *) let ctx_compute_variant_name (span : Meta.span) (ctx : extraction_ctx) (def_name : llbc_name) (variant : string) : string = - match !backend with + match backend () with | FStar | Coq | HOL4 -> let variant = to_camel_case variant in if !variant_concatenate_type_name then @@ -1465,14 +1465,14 @@ let ctx_compute_fun_name_no_suffix (span : Meta.span) (ctx : extraction_ctx) let fname = ctx_compute_simple_name span ctx fname in (* TODO: don't convert to snake case for Coq, HOL4, F* *) let fname = flatten_name fname in - match !backend with + match backend () with | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname | Lean -> fname (** Provided a basename, compute the name of a global declaration. *) let ctx_compute_global_name (span : Meta.span) (ctx : extraction_ctx) (name : llbc_name) : string = - match !Config.backend with + match Config.backend () with | Coq | FStar | HOL4 -> let parts = List.map to_snake_case (ctx_compute_simple_name span ctx name) @@ -1537,7 +1537,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl) trait_name_with_generics_to_simple_name ctx.trans_ctx name params args in let name = flatten_name name in - match !backend with + match backend () with | FStar -> StringUtils.lowercase_first_letter name | Coq | HOL4 | Lean -> name @@ -1614,7 +1614,7 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx) else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ clause in let clause = clause ^ "Inst" in - match !backend with + match backend () with | FStar -> StringUtils.lowercase_first_letter clause | Coq | HOL4 | Lean -> clause @@ -1633,7 +1633,7 @@ let ctx_compute_trait_type_name (ctx : extraction_ctx) (trait_decl : trait_decl) can't disambiguate fields coming from different ADTs if they have the same names), and thus don't need to add a prefix starting with a lowercase. *) - match !backend with FStar -> "t" ^ name | Coq | Lean | HOL4 -> name + match backend () with FStar -> "t" ^ name | Coq | Lean | HOL4 -> name let ctx_compute_trait_const_name (ctx : extraction_ctx) (trait_decl : trait_decl) (item : string) : string = @@ -1642,7 +1642,7 @@ let ctx_compute_trait_const_name (ctx : extraction_ctx) else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ item in (* See [trait_type_name] *) - match !backend with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name + match backend () with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name let ctx_compute_trait_method_name (ctx : extraction_ctx) (trait_decl : trait_decl) (item : string) : string = @@ -1677,7 +1677,7 @@ let ctx_compute_termination_measure_name (span : Meta.span) let lp_suffix = default_fun_loop_suffix num_loops loop_id in (* Compute the suffix *) let suffix = - match !Config.backend with + match Config.backend () with | FStar -> "_decreases" | Lean -> "_terminates" | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected" @@ -1706,7 +1706,7 @@ let ctx_compute_decreases_proof_name (span : Meta.span) (ctx : extraction_ctx) let lp_suffix = default_fun_loop_suffix num_loops loop_id in (* Compute the suffix *) let suffix = - match !Config.backend with + match Config.backend () with | Lean -> "_decreases" | FStar | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected" in @@ -1747,7 +1747,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx) match basename with | Some basename -> ( (* This should be a no-op *) - match !Config.backend with + match Config.backend () with | Lean -> basename | FStar | Coq | HOL4 -> to_snake_case basename) | None -> ( @@ -1779,7 +1779,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx) name_from_type_ident (TypesUtils.as_ident cl)) | TVar _ -> ( (* TODO: use "t" also for F* *) - match !backend with + match backend () with | FStar -> "x" (* lacking inspiration here... *) | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *)) | TLiteral lty -> ( @@ -1792,7 +1792,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx) let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) : string = (* Rust type variables are snake-case and start with a capital letter *) - match !backend with + match backend () with | FStar -> (* This is *not* a no-op: this removes the capital letter *) to_snake_case basename @@ -1805,7 +1805,7 @@ let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) : let ctx_compute_const_generic_var_basename (_ctx : extraction_ctx) (basename : string) : string = (* Rust type variables are snake-case and start with a capital letter *) - match !backend with + match backend () with | FStar | HOL4 -> (* This is *not* a no-op: this removes the capital letter *) to_snake_case basename @@ -1827,7 +1827,7 @@ let ctx_compute_trait_clause_basename (ctx : extraction_ctx) params.trait_clauses clause_id in let clause = clause ^ "Inst" in - match !backend with + match backend () with | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter clause | Lean -> clause diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index ff936d2f..37b676bb 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -43,13 +43,13 @@ let split_on_separator (s : string) : string list = Str.split (Str.regexp "\\(::\\|\\.\\)") s let flatten_name (name : string list) : string = - match !backend with + match backend () with | FStar | Coq | HOL4 -> String.concat "_" name | Lean -> String.concat "." name (** Utility for Lean-only definitions **) let mk_lean_only (funs : 'a list) : 'a list = - match !backend with Lean -> funs | _ -> [] + match backend () with Lean -> funs | _ -> [] let () = assert (split_on_separator "x::y::z" = [ "x"; "y"; "z" ]); @@ -61,7 +61,7 @@ let () = is F*, Coq or HOL4, and a different value if the target is Lean. *) let backend_choice (fstar_coq_hol4 : 'a) (lean : 'a) : 'a = - match !backend with Coq | FStar | HOL4 -> fstar_coq_hol4 | Lean -> lean + match backend () with Coq | FStar | HOL4 -> fstar_coq_hol4 | Lean -> lean let builtin_globals : (string * string) list = [ @@ -135,9 +135,11 @@ type type_variant_kind = let mk_struct_constructor (type_name : string) : string = let prefix = - match !backend with FStar -> "Mk" | Coq | HOL4 -> "mk" | Lean -> "" + match backend () with FStar -> "Mk" | Coq | HOL4 -> "mk" | Lean -> "" + in + let suffix = + match backend () with FStar | Coq | HOL4 -> "" | Lean -> ".mk" in - let suffix = match !backend with FStar | Coq | HOL4 -> "" | Lean -> ".mk" in prefix ^ type_name ^ suffix (** The assumed types. @@ -164,7 +166,7 @@ let builtin_types () : builtin_type_info list = List.map (fun (rname, name) -> ( rname, - match !backend with + match backend () with | FStar | Lean -> name | Coq | HOL4 -> extract_name ^ "_" ^ name )) fields @@ -197,7 +199,7 @@ let builtin_types () : builtin_type_info list = { rust_name = parse_pattern "core::option::Option"; extract_name = - (match !backend with + (match backend () with | Lean -> "Option" | Coq | FStar | HOL4 -> "option"); keep_params = None; @@ -208,7 +210,7 @@ let builtin_types () : builtin_type_info list = { rust_variant_name = "None"; extract_variant_name = - (match !backend with + (match backend () with | FStar | Coq -> "None" | Lean -> "none" | HOL4 -> "NONE"); @@ -217,7 +219,7 @@ let builtin_types () : builtin_type_info list = { rust_variant_name = "Some"; extract_variant_name = - (match !backend with + (match backend () with | FStar | Coq -> "Some" | Lean -> "some" | HOL4 -> "SOME"); @@ -529,7 +531,7 @@ let mk_builtin_fun_effects () : (pattern * effect_info) list = builtin_funs let mk_builtin_fun_effects_map () = - NameMatcherMap.of_list (mk_builtin_fun_effects ()) + NameMatcherMap.of_list (if_backend mk_builtin_fun_effects []) let builtin_fun_effects_map = mk_memoized mk_builtin_fun_effects_map @@ -571,7 +573,7 @@ let builtin_trait_decls_info () = else extract_name ^ "_" ^ item_name in let type_name = - match !backend with + match backend () with | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter type_name | Lean -> type_name in diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index cc0c351d..15e75da2 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -19,12 +19,12 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool) (cv : literal) : unit = match cv with | VScalar sv -> ( - match !backend with + match backend () with | FStar -> F.pp_print_string fmt (Z.to_string sv.value) | Coq | HOL4 | Lean -> - let print_brackets = inside && !backend = HOL4 in + let print_brackets = inside && backend () = HOL4 in if print_brackets then F.pp_print_string fmt "("; - (match !backend with + (match backend () with | Coq | Lean -> () | HOL4 -> F.pp_print_string fmt ("int_to_" ^ int_name sv.int_ty); @@ -34,7 +34,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool) if sv.value >= Z.of_int 0 then F.pp_print_string fmt (Z.to_string sv.value) else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")"); - (match !backend with + (match backend () with | Coq -> let iname = int_name sv.int_ty in F.pp_print_string fmt ("%" ^ iname) @@ -46,13 +46,13 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool) if print_brackets then F.pp_print_string fmt ")") | VBool b -> let b = - match !backend with + match backend () with | HOL4 -> if b then "T" else "F" | Coq | FStar | Lean -> if b then "true" else "false" in F.pp_print_string fmt b | VChar c -> ( - match !backend with + match backend () with | HOL4 -> (* [#"a"] is a notation for [CHR 97] (97 is the ASCII code for 'a') *) F.pp_print_string fmt ("#\"" ^ String.make 1 c ^ "\"") @@ -99,7 +99,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit) | Cast (src, tgt) -> ( (* HOL4 has a special treatment: because it doesn't support dependent types, we don't have a specific operator for the cast *) - match !backend with + match backend () with | HOL4 -> (* Casting, say, an u32 to an i32 would be done as follows: {[ @@ -121,7 +121,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit) (* Different cases depending on the conversion *) (let cast_str, src, tgt = let integer_type_to_string (ty : integer_type) : string = - if !backend = Lean then "." ^ int_name ty + if backend () = Lean then "." ^ int_name ty else StringUtils.capitalize_first_letter (PrintPure.integer_type_to_string ty) @@ -129,20 +129,20 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit) match (src, tgt) with | TInteger src, TInteger tgt -> let cast_str = - match !backend with + match backend () with | Coq | FStar -> "scalar_cast" | Lean -> "Scalar.cast" | HOL4 -> craise __FILE__ __LINE__ span "Unreachable" in let src = - if !backend <> Lean then Some (integer_type_to_string src) + if backend () <> Lean then Some (integer_type_to_string src) else None in let tgt = integer_type_to_string tgt in (cast_str, src, Some tgt) | TBool, TInteger tgt -> let cast_str = - match !backend with + match backend () with | Coq | FStar -> "scalar_cast_bool" | Lean -> "Scalar.cast_bool" | HOL4 -> craise __FILE__ __LINE__ span "Unreachable" @@ -198,7 +198,7 @@ let extract_binop (span : Meta.span) (arg0 : texpression) (arg1 : texpression) : unit = if inside then F.pp_print_string fmt "("; (* Some binary operations have a special notation depending on the backend *) - (match (!backend, binop) with + (match (backend (), binop) with | HOL4, (Eq | Ne) | (FStar | Coq | Lean), (Eq | Lt | Le | Ne | Ge | Gt) | Lean, (Div | Rem | Add | Sub | Mul | Shl | Shr | BitXor | BitOr | BitAnd) -> @@ -207,7 +207,7 @@ let extract_binop (span : Meta.span) | Eq -> "=" | Lt -> "<" | Le -> "<=" - | Ne -> if !backend = Lean then "!=" else "<>" + | Ne -> if backend () = Lean then "!=" else "<>" | Ge -> ">=" | Gt -> ">" | Div -> "/" @@ -225,7 +225,9 @@ let extract_binop (span : Meta.span) | BitAnd -> "&&&" in let binop = - match !backend with FStar | Lean | HOL4 -> binop | Coq -> "s" ^ binop + match backend () with + | FStar | Lean | HOL4 -> binop + | Coq -> "s" ^ binop in extract_expr false arg0; F.pp_print_space fmt (); @@ -239,7 +241,7 @@ let extract_binop (span : Meta.span) (* In the case of F*, for shift operations, because machine integers are simply integers with a refinement, if the second argument is a constant we need to provide the second implicit type argument *) - if binop_is_shift && !backend = FStar && is_const arg1 then ( + if binop_is_shift && backend () = FStar && is_const arg1 then ( F.pp_print_space fmt (); let ty = ty_as_integer span arg1.ty in F.pp_print_string fmt @@ -275,7 +277,7 @@ let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool = *) let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter) (is_rec : bool) (dg : Pure.fun_decl list) = - match !backend with + match backend () with | FStar | Coq | Lean -> () | HOL4 -> (* In HOL4, opaque functions have a special treatment *) @@ -304,7 +306,7 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter) (** See {!start_fun_decl_group}. *) let end_fun_decl_group (fmt : F.formatter) (is_rec : bool) (dg : Pure.fun_decl list) = - match !backend with + match backend () with | FStar -> () | Coq -> (* For aesthetic reasons, we print the Coq end group delimiter directly @@ -335,7 +337,7 @@ let end_fun_decl_group (fmt : F.formatter) (is_rec : bool) (** See {!start_fun_decl_group}: similar usage, but for the type declarations. *) let start_type_decl_group (ctx : extraction_ctx) (fmt : F.formatter) (is_rec : bool) (dg : Pure.type_decl list) = - match !backend with + match backend () with | FStar | Coq -> () | Lean -> if is_rec && List.length dg > 1 then ( @@ -362,7 +364,7 @@ let start_type_decl_group (ctx : extraction_ctx) (fmt : F.formatter) (** See {!start_fun_decl_group}. *) let end_type_decl_group (fmt : F.formatter) (is_rec : bool) (dg : Pure.type_decl list) = - match !backend with + match backend () with | FStar -> () | Coq -> (* For aesthetic reasons, we print the Coq end group delimiter directly @@ -394,11 +396,11 @@ let end_type_decl_group (fmt : F.formatter) (is_rec : bool) F.pp_print_break fmt 0 0) let unit_name () = - match !backend with Lean -> "Unit" | Coq | FStar | HOL4 -> "unit" + match backend () with Lean -> "Unit" | Coq | FStar | HOL4 -> "unit" (** Small helper *) let extract_arrow (fmt : F.formatter) () : unit = - if !Config.backend = Lean then F.pp_print_string fmt "→" + if Config.backend () = Lean then F.pp_print_string fmt "→" else F.pp_print_string fmt "->" let extract_const_generic (span : Meta.span) (ctx : extraction_ctx) @@ -441,7 +443,7 @@ let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter) *) let extract_ty_errors (fmt : F.formatter) : unit = - match !Config.backend with + match Config.backend () with | FStar | Coq -> F.pp_print_string fmt "admit" | Lean -> F.pp_print_string fmt "sorry" | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)" @@ -463,7 +465,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) (fun () -> F.pp_print_space fmt (); let product = - match !backend with + match backend () with | FStar -> "&" | Coq -> "*" | Lean -> "×" @@ -480,7 +482,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) In HOL4 we would write: `('a, 'b) tree` *) - match !backend with + match backend () with | FStar | Coq | Lean -> let print_paren = inside && has_params in if print_paren then F.pp_print_string fmt "("; @@ -556,7 +558,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) type_name ctx in let add_brackets (s : string) = - if !backend = Coq then "(" ^ s ^ ")" else s + if backend () = Coq then "(" ^ s ^ ")" else s in (* There may be a special treatment depending on the instance id. See the comments for {!extract_trait_instance_id_with_dot}. @@ -575,7 +577,9 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt type_name | _ -> (* HOL4 doesn't have 1st class types *) - cassert __FILE__ __LINE__ (!backend <> HOL4) span + cassert __FILE__ __LINE__ + (backend () <> HOL4) + span "Trait types are not supported yet when generating code for HOL4"; extract_trait_ref span ctx fmt no_params_tys false trait_ref; F.pp_print_string fmt ("." ^ add_brackets type_name)) @@ -624,14 +628,16 @@ and extract_generic_args (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (generics : generic_args) : unit = let { types; const_generics; trait_refs } = generics in - if !backend <> HOL4 then ( + if backend () <> HOL4 then ( if types <> [] then ( F.pp_print_space fmt (); Collections.List.iter_link (F.pp_print_space fmt) (extract_ty span ctx fmt no_params_tys true) types); if const_generics <> [] then ( - cassert __FILE__ __LINE__ (!backend <> HOL4) span + cassert __FILE__ __LINE__ + (backend () <> HOL4) + span "Constant generics are not supported yet when generating code for HOL4"; F.pp_print_space fmt (); Collections.List.iter_link (F.pp_print_space fmt) @@ -682,7 +688,9 @@ and extract_trait_instance_id_with_dot (span : Meta.span) (ctx : extraction_ctx) and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool) (id : trait_instance_id) : unit = - let add_brackets (s : string) = if !backend = Coq then "(" ^ s ^ ")" else s in + let add_brackets (s : string) = + if backend () = Coq then "(" ^ s ^ ")" else s + in match id with | Self -> (* This has a specific treatment depending on the item we're extracting @@ -812,7 +820,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : in (* Add the type name prefix for Lean *) let name = - if !Config.backend = Lean then + if Config.backend () = Lean then let type_name = ctx_compute_type_name def.span ctx def.llbc_name in @@ -859,7 +867,7 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx) (* [| Cons :] * Note that we really don't want any break above so we print everything * at once. *) - let opt_colon = if !backend <> HOL4 then " :" else "" in + let opt_colon = if backend () <> HOL4 then " :" else "" in F.pp_print_string fmt ("| " ^ cons_name ^ opt_colon); let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) : extraction_ctx = @@ -871,7 +879,7 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx) * Note that when printing fields, we register the field names as * *variables*: they don't need to be unique at the top level. *) let ctx = - match !backend with + match backend () with | FStar -> ( match f.field_name with | None -> ctx @@ -887,10 +895,10 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx) | Coq | Lean | HOL4 -> ctx in (* Print the field type *) - let inside = !backend = HOL4 in + let inside = backend () = HOL4 in extract_ty span ctx fmt type_decl_group inside f.field_ty; (* Print the arrow [->] *) - if !backend <> HOL4 then ( + if backend () <> HOL4 then ( F.pp_print_space fmt (); extract_arrow fmt ()); (* Close the field box *) @@ -904,9 +912,9 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx) List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields in (* Sanity check: HOL4 doesn't support const generics *) - sanity_check __FILE__ __LINE__ (cg_params = [] || !backend <> HOL4) span; + sanity_check __FILE__ __LINE__ (cg_params = [] || backend () <> HOL4) span; (* Print the final type *) - if !backend <> HOL4 then ( + if backend () <> HOL4 then ( F.pp_print_space fmt (); F.pp_open_hovbox fmt 0; F.pp_print_string fmt type_name; @@ -978,7 +986,7 @@ let extract_type_decl_tuple_struct_body (span : Meta.span) F.pp_print_space fmt (); F.pp_print_string fmt (unit_name ())) else - let sep = match !backend with Coq | FStar | HOL4 -> "*" | Lean -> "×" in + let sep = match backend () with Coq | FStar | HOL4 -> "*" | Lean -> "×" in Collections.List.iter_link (fun () -> F.pp_print_space fmt (); @@ -1049,28 +1057,28 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) (* Note that we already printed: [type t =] *) let is_rec = decl_is_from_rec_group kind in let _ = - if !backend = FStar && fields = [] then ( + if backend () = FStar && fields = [] then ( F.pp_print_space fmt (); F.pp_print_string fmt (unit_name ())) - else if !backend = Lean && fields = [] then () + else if backend () = Lean && fields = [] then () (* If the definition is recursive, we may need to extract it as an inductive (instead of a record). We start with the "normal" case: we extract it as a record. *) - else if (not is_rec) || (!backend <> Coq && !backend <> Lean) then ( - if !backend <> Lean then F.pp_print_space fmt (); + else if (not is_rec) || (backend () <> Coq && backend () <> Lean) then ( + if backend () <> Lean then F.pp_print_space fmt (); (* If Coq: print the constructor name *) (* TODO: remove superfluous test not is_rec below *) - if !backend = Coq && not is_rec then ( + if backend () = Coq && not is_rec then ( F.pp_print_string fmt (ctx_get_struct def.span (TAdtId def.def_id) ctx); F.pp_print_string fmt " "); - (match !backend with + (match backend () with | Lean -> () | FStar | Coq -> F.pp_print_string fmt "{" | HOL4 -> F.pp_print_string fmt "<|"); F.pp_print_break fmt 1 ctx.indent_incr; (* The body itself *) (* Open a box for the body *) - (match !backend with + (match backend () with | Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0 | Lean -> F.pp_open_vbox fmt 0); (* Print the fields *) @@ -1085,7 +1093,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt ":"; F.pp_print_space fmt (); extract_ty def.span ctx fmt type_decl_group false f.field_ty; - if !backend <> Lean then F.pp_print_string fmt ";"; + if backend () <> Lean then F.pp_print_string fmt ";"; (* Close the box for the field *) F.pp_close_box fmt () in @@ -1095,7 +1103,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) fields; (* Close the box for the body *) F.pp_close_box fmt (); - match !backend with + match backend () with | Lean -> () | FStar | Coq -> F.pp_print_space fmt (); @@ -1107,7 +1115,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) (* We extract for Coq or Lean, and we have a recursive record, or a record in a group of mutually recursive types: we extract it as an inductive type *) cassert __FILE__ __LINE__ - (is_rec && (!backend = Coq || !backend = Lean)) + (is_rec && (backend () = Coq || backend () = Lean)) def.span "Constant generics are not supported yet when generating code for HOL4"; (* Small trick: in Lean we use namespaces, meaning we don't need to prefix @@ -1115,7 +1123,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) i.e., instead of generating `inductive Foo := | MkFoo ...` like in Coq we generate `inductive Foo := | mk ... *) let cons_name = - if !backend = Lean then "mk" + if backend () = Lean then "mk" else ctx_get_struct def.span (TAdtId def.def_id) ctx in let def_name = ctx_get_local_type def.span def.def_id ctx in @@ -1128,7 +1136,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) let extract_comment (fmt : F.formatter) (sl : string list) : unit = (* Delimiters, space after we break a line *) let ld, space, rd = - match !backend with + match backend () with | Coq | FStar | HOL4 -> ("(** ", 4, " *)") | Lean -> ("/- ", 3, " -/") in @@ -1223,18 +1231,18 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx) let all_params = List.concat [ type_params; cg_params; trait_clauses ] in (* HOL4 doesn't support const generics *) cassert __FILE__ __LINE__ - (cg_params = [] || !backend <> HOL4) + (cg_params = [] || backend () <> HOL4) span "Constant generics are not supported yet when generating code for HOL4"; let left_bracket (implicit : bool) = - if implicit && !backend <> FStar then F.pp_print_string fmt "{" + if implicit && backend () <> FStar then F.pp_print_string fmt "{" else F.pp_print_string fmt "(" in let right_bracket (implicit : bool) = - if implicit && !backend <> FStar then F.pp_print_string fmt "}" + if implicit && backend () <> FStar then F.pp_print_string fmt "}" else F.pp_print_string fmt ")" in let print_implicit_symbol (implicit : bool) = - if implicit && !backend = FStar then F.pp_print_string fmt "#" else () + if implicit && backend () = FStar then F.pp_print_string fmt "#" else () in let insert_req_space () = match space with @@ -1254,7 +1262,7 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx) (const_generics : const_generic_var list) (trait_clauses : trait_clause list) : unit = (* Note that in HOL4 we don't print the type parameters. *) - if !backend <> HOL4 then ( + if backend () <> HOL4 then ( (* Print the type parameters *) if type_params <> [] then ( insert_req_space (); @@ -1372,7 +1380,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl) (extract_body : bool) : unit = (* Sanity check *) - sanity_check __FILE__ __LINE__ (extract_body || !backend <> HOL4) def.span; + sanity_check __FILE__ __LINE__ (extract_body || backend () <> HOL4) def.span; let is_tuple_struct = TypesUtils.type_decl_from_decl_id_is_tuple_struct ctx.trans_ctx.type_ctx.type_infos def.def_id @@ -1397,7 +1405,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) The boolean [is_opaque_coq] is used to detect this case. *) let is_opaque = type_kind = None in - let is_opaque_coq = !backend = Coq && is_opaque in + let is_opaque_coq = backend () = Coq && is_opaque in let use_forall = is_opaque_coq && def.generics <> empty_generic_params in (* Retrieve the definition name *) let def_name = ctx_get_local_type def.span def.def_id ctx in @@ -1408,7 +1416,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) ctx in (* Add a break before *) - if !backend <> HOL4 || not (decl_is_first_from_group kind) then + if backend () <> HOL4 || not (decl_is_first_from_group kind) then F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) (let name = @@ -1423,7 +1431,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* Open a box for the definition, so that whenever possible it gets printed on * one line. Note however that in the case of Lean line breaks are important * for parsing: we thus use a hovbox. *) - (match !backend with + (match backend () with | Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0 | Lean -> if is_tuple_struct then F.pp_open_hvbox fmt 0 else F.pp_open_vbox fmt 0); @@ -1433,7 +1441,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) We need this annotation, otherwise Lean sometimes doesn't manage to typecheck the expressions when it needs to coerce the type. *) - if is_tuple_struct_one_or_zero_field && !backend = Lean then ( + if is_tuple_struct_one_or_zero_field && backend () = Lean then ( F.pp_print_string fmt "@[reducible]"; F.pp_print_space fmt ()) else (); @@ -1445,7 +1453,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* HOL4 doesn't support const generics, and type definitions in HOL4 don't support trait clauses *) cassert __FILE__ __LINE__ - ((cg_params = [] && trait_clauses = []) || !backend <> HOL4) + ((cg_params = [] && trait_clauses = []) || backend () <> HOL4) def.span "Constant generics and type definitions with trait clauses are not \ supported yet when generating code for HOL4"; @@ -1456,7 +1464,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) if extract_body then ( F.pp_print_space fmt (); let eq = - match !backend with + match backend () with | FStar -> "=" | Coq -> (* For Coq, the `*` is overloaded. If we want to extract a product @@ -1493,10 +1501,10 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) type_params cg_params variants | Opaque -> craise __FILE__ __LINE__ def.span "Unreachable"); (* Add the definition end delimiter *) - if !backend = HOL4 && decl_is_not_last_from_group kind then ( + if backend () = HOL4 && decl_is_not_last_from_group kind then ( F.pp_print_space fmt (); F.pp_print_string fmt ";") - else if !backend = Coq && decl_is_last_from_group kind then ( + else if backend () = Coq && decl_is_last_from_group kind then ( (* This is actually an end of group delimiter. For aesthetic reasons we print it here instead of in {!end_type_decl_group}. *) F.pp_print_cut fmt (); @@ -1504,7 +1512,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* Close the box for the definition *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) - if !backend <> HOL4 || decl_is_not_last_from_group kind then + if backend () <> HOL4 || decl_is_not_last_from_group kind then F.pp_print_break fmt 0 0 (** Extract an opaque type declaration to HOL4. @@ -1572,11 +1580,11 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) | Assumed | Declared -> false in if extract_body then - if !backend = HOL4 && is_empty_record_type_decl def then + if backend () = HOL4 && is_empty_record_type_decl def then extract_type_decl_hol4_empty_record ctx fmt def else extract_type_decl_gen ctx fmt type_decl_group kind def extract_body else - match !backend with + match backend () with | FStar | Coq | Lean -> extract_type_decl_gen ctx fmt type_decl_group kind def extract_body | HOL4 -> extract_type_decl_hol4_opaque ctx fmt def @@ -1625,7 +1633,7 @@ let extract_coq_arguments_instruction (ctx : extraction_ctx) (fmt : F.formatter) *) let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = - sanity_check __FILE__ __LINE__ (!backend = Coq) decl.span; + sanity_check __FILE__ __LINE__ (backend () = Coq) decl.span; (* Generating the [Arguments] instructions is useful only if there are parameters *) let num_params = List.length decl.generics.types @@ -1674,7 +1682,9 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) *) let extract_type_decl_record_field_projectors (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = - sanity_check __FILE__ __LINE__ (!backend = Coq || !backend = Lean) decl.span; + sanity_check __FILE__ __LINE__ + (backend () = Coq || backend () = Lean) + decl.span; match decl.kind with | Opaque | Enum _ -> () | Struct fields -> @@ -1704,7 +1714,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) F.pp_open_hvbox fmt ctx.indent_incr; (* For Lean: add some attributes *) - if !backend = Lean then ( + if backend () = Lean then ( (* Box for the attributes *) F.pp_open_vbox fmt 0; (* Annotate the projectors with both simp and reducible. @@ -1717,7 +1727,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) (* Box for the [def ADT.proj ... :=] *) F.pp_open_hovbox fmt ctx.indent_incr; - (match !backend with + (match backend () with | Lean -> F.pp_print_string fmt "def" | Coq -> F.pp_print_string fmt "Definition" | _ -> internal_error __FILE__ __LINE__ decl.span); @@ -1729,7 +1739,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) let field_name = ctx_get_field decl.span (TAdtId decl.def_id) field_id ctx in - if !backend = Lean then ( + if backend () = Lean then ( F.pp_print_string fmt def_name; F.pp_print_string fmt "."); F.pp_print_string fmt field_name; @@ -1795,7 +1805,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) F.pp_close_box fmt (); (* Print the [end] *) - if !backend = Coq then ( + if backend () = Coq then ( F.pp_print_space fmt (); F.pp_print_string fmt "end"); @@ -1804,7 +1814,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) (* Close the inner box projector *) F.pp_close_box fmt (); (* If Coq: end the definition with a "." *) - if !backend = Coq then ( + if backend () = Coq then ( F.pp_print_cut fmt (); F.pp_print_string fmt "."); (* Close the outer box for projector definition *) @@ -1842,7 +1852,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) (* Close the inner box projector *) F.pp_close_box fmt (); (* If Coq: end the definition with a "." *) - if !backend = Coq then ( + if backend () = Coq then ( F.pp_print_cut fmt (); F.pp_print_string fmt "."); (* Close the outer box projector *) @@ -1854,7 +1864,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) let extract_field_proj_and_notation (field_id : FieldId.id) (field : field) : unit = extract_field_proj field_id field; - if !backend = Coq then extract_proj_notation field_id field + if backend () = Coq then extract_proj_notation field_id field in FieldId.iteri extract_field_proj_and_notation fields @@ -1866,7 +1876,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) *) let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = - match !backend with + match backend () with | FStar | HOL4 -> () | Lean | Coq -> if @@ -1874,7 +1884,8 @@ let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter) (TypesUtils.type_decl_from_decl_id_is_tuple_struct ctx.trans_ctx.type_ctx.type_infos decl.def_id) then ( - if !backend = Coq then extract_type_decl_coq_arguments ctx fmt kind decl; + if backend () = Coq then + extract_type_decl_coq_arguments ctx fmt kind decl; extract_type_decl_record_field_projectors ctx fmt kind decl) (** Extract the state type declaration. *) @@ -1893,7 +1904,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) (* The syntax for Lean and Coq is almost identical. *) let print_axiom () = let axiom = - match !backend with + match backend () with | Coq -> "Axiom" | Lean -> "axiom" | FStar | HOL4 -> raise (Failure "Unexpected") @@ -1905,14 +1916,14 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) F.pp_print_string fmt ":"; F.pp_print_space fmt (); F.pp_print_string fmt "Type"; - if !backend = Coq then F.pp_print_string fmt "." + if backend () = Coq then F.pp_print_string fmt "." in (* The kind should be [Assumed] or [Declared] *) (match kind with | SingleNonRec | SingleRec | MutRecFirst | MutRecInner | MutRecLast -> raise (Failure "Unexpected") | Assumed -> ( - match !backend with + match backend () with | FStar -> F.pp_print_string fmt "assume"; F.pp_print_space fmt (); @@ -1927,7 +1938,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) F.pp_print_string fmt ("val _ = new_type (\"" ^ state_name ^ "\", 0)") | Coq | Lean -> print_axiom ()) | Declared -> ( - match !backend with + match backend () with | FStar -> F.pp_print_string fmt "val"; F.pp_print_space fmt (); diff --git a/compiler/Main.ml b/compiler/Main.ml index 29322049..557a3993 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 diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index a4319b28..a22a39ab 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -649,7 +649,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl = (* Convert, if possible - note that for now for Lean and Coq we don't support the structure syntax on recursive structures *) if - (!Config.backend <> Lean && !Config.backend <> Coq) + (Config.backend () <> Lean && Config.backend () <> Coq) || not is_rec then let struct_id = TAdtId adt_id in @@ -1295,7 +1295,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl = the shape [{ x with f := v }]). This is not supported by Coq *) - !Config.backend <> Coq + Config.backend () <> Coq then ( (* Compute the number of occurrences of each variable *) let occurs = ref VarId.Map.empty in diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index e7dcd933..fe5d3414 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -241,7 +241,7 @@ let rec let_group_requires_parentheses (span : Meta.span) (e : texpression) : msg (* TODO : check if true should'nt be returned instead ? *) let texpression_requires_parentheses span e = - match !Config.backend with + match Config.backend () with | FStar | Lean -> false | Coq | HOL4 -> let_group_requires_parentheses span e diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 848bfe50..ba6bba68 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3693,7 +3693,7 @@ let wrap_in_match_fuel (span : Meta.span) (fuel0 : VarId.id) (fuel : VarId.id) let fail_branch = mk_result_fail_texpression_with_error_id span error_out_of_fuel_id body.ty in - match !Config.backend with + match Config.backend () with | FStar -> (* Generate an expression: {[ diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 0f887ec8..690bff5c 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -665,7 +665,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let extract_decrease decl = let has_decr_clause = has_decreases_clause decl in if has_decr_clause then - match !Config.backend with + match Config.backend () with | Lean -> Extract.extract_template_lean_termination_and_decreasing ctx fmt decl @@ -864,7 +864,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) * internal count is consistent with the state of the file. *) (* Create the header *) - (match !Config.backend with + (match Config.backend () with | Lean -> Printf.fprintf out "-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS\n"; Printf.fprintf out "-- [%s]%s\n" fi.rust_module_name fi.custom_msg @@ -873,7 +873,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n"; Printf.fprintf out "(** [%s]%s *)\n" fi.rust_module_name fi.custom_msg); (* Generate the imports *) - (match !Config.backend with + (match Config.backend () with | FStar -> Printf.fprintf out "module %s\n" fi.module_name; Printf.fprintf out "open Primitives\n"; @@ -957,7 +957,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) Format.pp_print_newline fmt (); (* Close the module *) - (match !Config.backend with + (match Config.backend () with | FStar -> () | Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n" @@ -1039,7 +1039,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : trans_ctx; names_maps; indent_incr = 2; - use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses; + use_dep_ite = + Config.backend () = Lean && !Config.extract_decreases_clauses; trait_decl_id = None (* None by default *); is_provided_method = false (* false by default *); trans_trait_decls; @@ -1113,13 +1114,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* Convert the case *) let crate_name = StringUtils.to_camel_case basename in let crate_name = - if !Config.backend = HOL4 then + if Config.backend () = HOL4 then StringUtils.lowercase_first_letter crate_name else crate_name in (* We use the raw crate name for the namespaces *) let namespace = - match !Config.backend with + match Config.backend () with | FStar | Coq | HOL4 -> crate.name | Lean -> crate.name in @@ -1144,7 +1145,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* Lean reflects the module hierarchy within the filesystem, so we need to create more directories *) - if !Config.backend = Lean then ( + if Config.backend () = Lean then ( let ( ^^ ) = Filename.concat in if !Config.split_files then mkdir_if (dest_dir ^^ crate_name); if needs_clauses_module then ( @@ -1156,7 +1157,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* Retrieve the executable's directory *) let exe_dir = Filename.dirname Sys.argv.(0) in let primitives_src_dest = - match !Config.backend with + match Config.backend () with | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst") | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v") | Lean -> None @@ -1190,18 +1191,18 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* Extract the file(s) *) let module_delimiter = - match !Config.backend with + match Config.backend () with | FStar -> "." | Coq -> "_" | Lean -> "." | HOL4 -> "_" in let file_delimiter = - if !Config.backend = Lean then "/" else module_delimiter + if Config.backend () = Lean then "/" else module_delimiter in (* File extension for the "regular" modules *) let ext = - match !Config.backend with + match Config.backend () with | FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" @@ -1209,7 +1210,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : in (* File extension for the opaque module *) let opaque_ext = - match !Config.backend with + match Config.backend () with | FStar -> ".fsti" | Coq -> ".v" | Lean -> ".lean" @@ -1253,7 +1254,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : For the other backends, we generate a template file as a model for the file the user has to provide. *) let module_suffix, opaque_imported_suffix, custom_msg = - match !Config.backend with + match Config.backend () with | FStar -> ("TypesExternal", "TypesExternal", ": external type declarations") | HOL4 | Coq | Lean -> @@ -1306,7 +1307,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* Extract the non opaque types *) let types_filename_ext = - match !Config.backend with + match Config.backend () with | FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" @@ -1377,7 +1378,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : For the other backends, we generate a template file as a model for the file the user has to provide. *) let module_suffix, opaque_imported_suffix, custom_msg = - match !Config.backend with + match Config.backend () with | FStar -> ( "FunsExternal", "FunsExternal", @@ -1445,7 +1446,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : let clauses_module = if needs_clauses_module then let clauses_submodule = - if !Config.backend = Lean then module_delimiter ^ "Clauses" else "" + if Config.backend () = Lean then module_delimiter ^ "Clauses" else "" in [ crate_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ] else [] @@ -1501,7 +1502,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : extract_file gen_config ctx file_info); (* Generate the build file *) - match !Config.backend with + match Config.backend () with | Coq | FStar | HOL4 -> () (* Nothing to do - TODO: we might want to generate the _CoqProject file for Coq. -- cgit v1.2.3 From 49c8e42ec3bcfc323e61c5ba0345abeb41372ac4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jun 2024 14:50:21 +0200 Subject: Implement a BorrowCheck.borrow_check_crate --- compiler/BorrowCheck.ml | 28 ++++++++++++++++++++++++++++ compiler/Interpreter.ml | 18 +++++++++++++----- compiler/Logging.ml | 3 +++ compiler/Main.ml | 9 ++++++--- compiler/Translate.ml | 5 +++-- compiler/dune | 1 + 6 files changed, 54 insertions(+), 10 deletions(-) create mode 100644 compiler/BorrowCheck.ml (limited to 'compiler') 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 -- cgit v1.2.3 From a6c9ab139977982f610f3d46e2e2f4c141880c3c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jun 2024 16:12:15 +0200 Subject: Relax some constraints in the symbolic execution when borrow-checking --- compiler/Interpreter.ml | 36 ++++++++++++++++++++++++++++------ compiler/InterpreterLoopsFixedPoint.ml | 26 ++++++++++++++++-------- compiler/InterpreterLoopsMatchCtxs.ml | 5 ++++- compiler/Print.ml | 3 ++- 4 files changed, 54 insertions(+), 16 deletions(-) (limited to 'compiler') diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 81d6ff72..b2e55841 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -362,6 +362,11 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) ctx) else ctx in + log#ldebug + (lazy + ("evaluate_function_symbolic_synthesize_backward_from_return: (after \ + putting the return value in the proper abstraction)\n" ^ "\n- ctx:\n" + ^ Print.Contexts.eval_ctx_to_string ~span:(Some fdef.item_meta.span) ctx)); (* We now need to end the proper *input* abstractions - pay attention * to the fact that we end the *input* abstractions, not the *return* @@ -418,7 +423,28 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) } ]} *) - (None, false) + (* If we are borrow-checking: end the synth input abstraction to + check there is no borrow-checking issue. + Otherwise, do nothing. + + We need this check because of the following: + {[ + fn loop_reborrow_mut1<'a, 'b>(a: &'a mut u32, b: &'b mut u32) -> &'a mut u32 { + let mut x = 0; + while x > 0 { + x += 1; + } + if x > 0 { + a + } else { + b // Failure + } + } + ]} + (remark: this is slightly ad-hoc, and we won't need to do that + once we make the handling of loops more general). + *) + if !Config.borrow_check then (Some fun_abs_id, true) else (None, false) | Some abs -> (Some abs.abs_id, false) in log#ldebug @@ -619,11 +645,9 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) let ctx_resl, cc = eval_function_body config (Option.get fdef.body).body ctx in - if synthesize then - (* Finish synthesizing *) - let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in - Some (cc el) - else None + let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in + (* Finish synthesizing *) + if synthesize then Some (cc el) else None with CFailure (span, msg) -> if synthesize then Some (Error (span, msg)) else None in diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 735f3743..0d770e80 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -665,8 +665,8 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) in List.iter end_at_return (fst (eval_loop_body fp)); - (* Check that the sets of abstractions we need to end per region group are pairwise - * disjoint *) + (* Check that the sets of abstractions we need to end per region group are + pairwise disjoint *) let aids_union = ref AbstractionId.Set.empty in let _ = RegionGroupId.Map.iter @@ -680,8 +680,10 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) !fp_ended_aids in - (* We also check that all the regions need to end - this is not necessary per - se, but if it doesn't happen it is bizarre and worth investigating... *) + (* If we generate a translation, we check that all the regions need to end + - this is not necessary per se, but if it doesn't happen it is bizarre and worth investigating... + We need this check for now for technical reasons to make the translation work. + *) sanity_check __FILE__ __LINE__ (AbstractionId.Set.equal !aids_union !fp_aids) span; @@ -779,9 +781,11 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) no region group, and we set them as endable just above). If [remove_rg_id] is [false], we simply set the abstractions as non-endable - to freeze them (we will use the fixed point as starting point for the - symbolic execution of the loop body, and we have to make sure the input - abstractions are frozen). + **when generating a pure translation** to freeze them (we will use the + fixed point as starting point for the symbolic execution of the loop body, + and we have to make sure the input abstractions are frozen). + If we are simply borrow-checking the program, we can set the abstraction + as endable. *) let update_loop_abstractions (remove_rg_id : bool) = object @@ -796,7 +800,13 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) if remove_rg_id then Loop (loop_id, None, LoopSynthInput) else abs.kind in - { abs with can_end = remove_rg_id; kind } + (* If we borrow check we can always set the abstraction as + endable. If we generate a pure translation we have a few + more constraints. *) + let can_end = + if !Config.borrow_check then true else remove_rg_id + in + { abs with can_end; kind } | _ -> abs end in diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 3f7c023e..a1c0841a 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -1956,7 +1956,10 @@ let match_ctx_with_target (config : config) (span : Meta.span) | Loop (loop_id', rg_id, kind) -> sanity_check __FILE__ __LINE__ (loop_id' = loop_id) span; sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) span; - let can_end = false in + (* If we borrow-check: we can set the abstractions as endable. + If we synthesize we have to constrain the region abstractions + a bit. *) + let can_end = !Config.borrow_check in let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in let abs = { abs with kind; can_end } in super#visit_abs env abs diff --git a/compiler/Print.ml b/compiler/Print.ml index 7495d6bf..8bd709d0 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -309,13 +309,14 @@ module Values = struct let kind = if verbose then "[kind:" ^ abs_kind_to_string abs.kind ^ "]" else "" in + let can_end = if abs.can_end then "{endable}" else "{frozen}" in indent ^ "abs@" ^ AbstractionId.to_string abs.abs_id ^ kind ^ "{parents=" ^ AbstractionId.Set.to_string None abs.parents ^ "}" ^ "{regions=" ^ RegionId.Set.to_string None abs.regions - ^ "}" ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}" + ^ "}" ^ can_end ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}" let inst_fun_sig_to_string (env : fmt_env) (sg : LlbcAst.inst_fun_sig) : string = -- cgit v1.2.3 From 0a0ab7c0e159e736a3187b8121d106ee76651f57 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jun 2024 16:47:52 +0200 Subject: Relax more checks for borrow-checking --- compiler/InterpreterLoopsFixedPoint.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'compiler') diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 0d770e80..3760d15a 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -683,9 +683,10 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) (* If we generate a translation, we check that all the regions need to end - this is not necessary per se, but if it doesn't happen it is bizarre and worth investigating... We need this check for now for technical reasons to make the translation work. + If we only borrow-check, we can ignore this. *) sanity_check __FILE__ __LINE__ - (AbstractionId.Set.equal !aids_union !fp_aids) + (!Config.borrow_check || AbstractionId.Set.equal !aids_union !fp_aids) span; (* Merge the abstractions which need to be merged, and compute the map from -- cgit v1.2.3 From 7cb0914c68a055a308539ccc781fea8f30ef27bb Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jun 2024 17:03:57 +0200 Subject: Update an error message --- compiler/InterpreterPaths.ml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'compiler') diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 8a924a0a..992146de 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -250,12 +250,16 @@ let rec access_projection (span : Meta.span) (access : projection_access) Ok (ctx, { res with updated = nv }) else Error (FailSharedLoan bids)) | (_, (VLiteral _ | VAdt _ | VBottom | VBorrow _), _) as r -> - let pe, v, ty = r in - let pe = "- pe: " ^ show_projection_elem pe in - let v = "- v:\n" ^ show_value v in - let ty = "- ty:\n" ^ show_ety ty in - craise __FILE__ __LINE__ span - ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty)) + if v.value = VBottom then + craise __FILE__ __LINE__ span + "Can not apply a projection to the ⊥ value" + else + let pe, v, ty = r in + let pe = "- pe: " ^ show_projection_elem pe in + let v = "- v:\n" ^ show_value v in + let ty = "- ty:\n" ^ show_ety ty in + craise __FILE__ __LINE__ span + ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty)) (** Generic function to access (read/write) the value at a given place. -- cgit v1.2.3 From 0892b943de4de5e34372b91b40580e5bdfe50016 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jun 2024 17:48:46 +0200 Subject: Fix a minor issue --- compiler/ExtractBase.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'compiler') diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 3346c328..bc56dd28 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -850,6 +850,7 @@ let keywords () = "assert_norm"; "assume"; "else"; + "end"; "fun"; "fn"; "FStar"; -- cgit v1.2.3 From e6d04cf1a73533ae80a68d9ef5f34a9e832e77a3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jun 2024 17:51:24 +0200 Subject: Fix a minor issue --- compiler/ExtractBase.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'compiler') diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index bc56dd28..4aac270f 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -883,6 +883,7 @@ let keywords () = "Declare"; "Definition"; "else"; + "end"; "End"; "fun"; "Fixpoint"; -- cgit v1.2.3