From 55998324442ed6c64543907425c1f4fedf8d7380 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 3 Jul 2024 11:24:32 +0200 Subject: [PATCH 01/10] Update charon --- charon-pin | 2 +- flake.lock | 12 ++-- scripts/update-charon-pin.sh | 3 + tests/coq/betree/Betree_Funs.v | 64 +++++++++---------- .../fstar/betree/Betree.Clauses.Template.fst | 14 ++-- tests/fstar/betree/Betree.Funs.fst | 46 ++++++------- tests/lean/Betree/Funs.lean | 44 ++++++------- 7 files changed, 94 insertions(+), 91 deletions(-) diff --git a/charon-pin b/charon-pin index 645a5ad7..afc5bfae 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -aeeae1d46704810bf498db552a75dff15aa3abcc +e0bf68d674edbb154fe2343b2315ccac325a0c7a diff --git a/flake.lock b/flake.lock index 6772358d..8ee72978 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1719829160, - "narHash": "sha256-M9APcqyQtLfteKUqePDt+jgio4OzQ7EvRuBwXgkCQWA=", + "lastModified": 1719994894, + "narHash": "sha256-RhSc57vv/xORPkjqnL4jcupcyV6DTfgm8KqRiOI1ruA=", "owner": "aeneasverif", "repo": "charon", - "rev": "aeeae1d46704810bf498db552a75dff15aa3abcc", + "rev": "e0bf68d674edbb154fe2343b2315ccac325a0c7a", "type": "github" }, "original": { @@ -272,11 +272,11 @@ ] }, "locked": { - "lastModified": 1719454714, - "narHash": "sha256-MojqG0lyUINkEk0b3kM2drsU5vyaF8DFZe/FAlZVOGs=", + "lastModified": 1719973106, + "narHash": "sha256-IGCdN/m7DfwUfxZjFnlTiTtpwSHCb01P/LWavAKD2jw=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "d1c527659cf076ecc4b96a91c702d080b213801e", + "rev": "fb733500aead50880b9b301f34a0061bf997d6f2", "type": "github" }, "original": { diff --git a/scripts/update-charon-pin.sh b/scripts/update-charon-pin.sh index 304b2d83..eadf6a1d 100755 --- a/scripts/update-charon-pin.sh +++ b/scripts/update-charon-pin.sh @@ -12,6 +12,9 @@ else echo 'Pinning the latest commit from Charon `main`' nix flake lock --update-input charon fi +# In both cases we also update the rust overlay to make sure we can get the +# latest rust nightlies. +nix flake lock --update-input charon/rust-overlay # Keep the commit revision in `./charon-pin` as well so that non-nix users can know which commit to use. echo '# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.' > ./charon-pin diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v index 9cbeb9a8..4eb29125 100644 --- a/tests/coq/betree/Betree_Funs.v +++ b/tests/coq/betree/Betree_Funs.v @@ -314,38 +314,6 @@ Definition betree_Node_lookup_first_message_for_key betree_Node_lookup_first_message_for_key_loop n key msgs . -(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0: - Source: 'src/betree.rs', lines 649:4-660:5 *) -Fixpoint betree_Node_lookup_in_bindings_loop - (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : - result (option u64) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match bindings with - | Betree_List_Cons hd tl => - let (i, i1) := hd in - if i s= key - then Ok (Some i1) - else - if i s> key - then Ok None - else betree_Node_lookup_in_bindings_loop n1 key tl - | Betree_List_Nil => Ok None - end - end -. - -(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: - Source: 'src/betree.rs', lines 649:4-649:84 *) -Definition betree_Node_lookup_in_bindings - (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : - result (option u64) - := - betree_Node_lookup_in_bindings_loop n key bindings -. - (** [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0: Source: 'src/betree.rs', lines 820:4-844:5 *) Fixpoint betree_Node_apply_upserts_loop @@ -388,6 +356,38 @@ Definition betree_Node_apply_upserts betree_Node_apply_upserts_loop n msgs prev key . +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 649:4-660:5 *) +Fixpoint betree_Node_lookup_in_bindings_loop + (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : + result (option u64) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match bindings with + | Betree_List_Cons hd tl => + let (i, i1) := hd in + if i s= key + then Ok (Some i1) + else + if i s> key + then Ok None + else betree_Node_lookup_in_bindings_loop n1 key tl + | Betree_List_Nil => Ok None + end + end +. + +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: + Source: 'src/betree.rs', lines 649:4-649:84 *) +Definition betree_Node_lookup_in_bindings + (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : + result (option u64) + := + betree_Node_lookup_in_bindings_loop n key bindings +. + (** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 414:4-414:63 *) Fixpoint betree_Internal_lookup_in_children diff --git a/tests/fstar/betree/Betree.Clauses.Template.fst b/tests/fstar/betree/Betree.Clauses.Template.fst index dbbfae2b..fcccedcc 100644 --- a/tests/fstar/betree/Betree.Clauses.Template.fst +++ b/tests/fstar/betree/Betree.Clauses.Template.fst @@ -42,13 +42,6 @@ let betree_Node_lookup_first_message_for_key_loop_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: decreases clause - Source: 'src/betree.rs', lines 649:4-660:5 *) -unfold -let betree_Node_lookup_in_bindings_loop_decreases (key : u64) - (bindings : betree_List_t (u64 & u64)) : nat = - admit () - (** [betree::betree::{betree::betree::Node#5}::apply_upserts]: decreases clause Source: 'src/betree.rs', lines 820:4-844:5 *) unfold @@ -57,6 +50,13 @@ let betree_Node_apply_upserts_loop_decreases (key : u64) : nat = admit () +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: decreases clause + Source: 'src/betree.rs', lines 649:4-660:5 *) +unfold +let betree_Node_lookup_in_bindings_loop_decreases (key : u64) + (bindings : betree_List_t (u64 & u64)) : nat = + admit () + (** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: decreases clause Source: 'src/betree.rs', lines 414:4-414:63 *) unfold diff --git a/tests/fstar/betree/Betree.Funs.fst b/tests/fstar/betree/Betree.Funs.fst index 53356bdb..6f543fb2 100644 --- a/tests/fstar/betree/Betree.Funs.fst +++ b/tests/fstar/betree/Betree.Funs.fst @@ -260,29 +260,6 @@ let betree_Node_lookup_first_message_for_key = betree_Node_lookup_first_message_for_key_loop key msgs -(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0: - Source: 'src/betree.rs', lines 649:4-660:5 *) -let rec betree_Node_lookup_in_bindings_loop - (key : u64) (bindings : betree_List_t (u64 & u64)) : - Tot (result (option u64)) - (decreases (betree_Node_lookup_in_bindings_loop_decreases key bindings)) - = - begin match bindings with - | Betree_List_Cons hd tl -> - let (i, i1) = hd in - if i = key - then Ok (Some i1) - else - if i > key then Ok None else betree_Node_lookup_in_bindings_loop key tl - | Betree_List_Nil -> Ok None - end - -(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: - Source: 'src/betree.rs', lines 649:4-649:84 *) -let betree_Node_lookup_in_bindings - (key : u64) (bindings : betree_List_t (u64 & u64)) : result (option u64) = - betree_Node_lookup_in_bindings_loop key bindings - (** [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0: Source: 'src/betree.rs', lines 820:4-844:5 *) let rec betree_Node_apply_upserts_loop @@ -319,6 +296,29 @@ let betree_Node_apply_upserts = betree_Node_apply_upserts_loop msgs prev key +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 649:4-660:5 *) +let rec betree_Node_lookup_in_bindings_loop + (key : u64) (bindings : betree_List_t (u64 & u64)) : + Tot (result (option u64)) + (decreases (betree_Node_lookup_in_bindings_loop_decreases key bindings)) + = + begin match bindings with + | Betree_List_Cons hd tl -> + let (i, i1) = hd in + if i = key + then Ok (Some i1) + else + if i > key then Ok None else betree_Node_lookup_in_bindings_loop key tl + | Betree_List_Nil -> Ok None + end + +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: + Source: 'src/betree.rs', lines 649:4-649:84 *) +let betree_Node_lookup_in_bindings + (key : u64) (bindings : betree_List_t (u64 & u64)) : result (option u64) = + betree_Node_lookup_in_bindings_loop key bindings + (** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 414:4-414:63 *) let rec betree_Internal_lookup_in_children diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean index dd8dfb05..bb2c0609 100644 --- a/tests/lean/Betree/Funs.lean +++ b/tests/lean/Betree/Funs.lean @@ -259,28 +259,6 @@ def betree.Node.lookup_first_message_for_key := betree.Node.lookup_first_message_for_key_loop key msgs -/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0: - Source: 'src/betree.rs', lines 649:4-660:5 -/ -divergent def betree.Node.lookup_in_bindings_loop - (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := - match bindings with - | betree.List.Cons hd tl => - let (i, i1) := hd - if i = key - then Result.ok (some i1) - else - if i > key - then Result.ok none - else betree.Node.lookup_in_bindings_loop key tl - | betree.List.Nil => Result.ok none - -/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: - Source: 'src/betree.rs', lines 649:4-649:84 -/ -@[reducible] -def betree.Node.lookup_in_bindings - (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := - betree.Node.lookup_in_bindings_loop key bindings - /- [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0: Source: 'src/betree.rs', lines 820:4-844:5 -/ divergent def betree.Node.apply_upserts_loop @@ -320,6 +298,28 @@ def betree.Node.apply_upserts := betree.Node.apply_upserts_loop msgs prev key +/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 649:4-660:5 -/ +divergent def betree.Node.lookup_in_bindings_loop + (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := + match bindings with + | betree.List.Cons hd tl => + let (i, i1) := hd + if i = key + then Result.ok (some i1) + else + if i > key + then Result.ok none + else betree.Node.lookup_in_bindings_loop key tl + | betree.List.Nil => Result.ok none + +/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: + Source: 'src/betree.rs', lines 649:4-649:84 -/ +@[reducible] +def betree.Node.lookup_in_bindings + (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := + betree.Node.lookup_in_bindings_loop key bindings + /- [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 414:4-414:63 -/ mutual divergent def betree.Internal.lookup_in_children From d413916d6fbc7c49bbf8e93518ed7bd454993a1c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 25 Jun 2024 14:02:13 +0200 Subject: [PATCH 02/10] Tweak formatting options --- compiler/.ocamlformat | 6 +++++- tests/test_runner/.ocamlformat | 5 +++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/compiler/.ocamlformat b/compiler/.ocamlformat index b0ae150e..f886c99f 100644 --- a/compiler/.ocamlformat +++ b/compiler/.ocamlformat @@ -1 +1,5 @@ -doc-comments=before \ No newline at end of file +break-cases = fit-or-vertical +doc-comments = before +exp-grouping = preserve +parens-tuple = always +parens-tuple-patterns = multi-line-only diff --git a/tests/test_runner/.ocamlformat b/tests/test_runner/.ocamlformat index e69de29b..077ddd51 100644 --- a/tests/test_runner/.ocamlformat +++ b/tests/test_runner/.ocamlformat @@ -0,0 +1,5 @@ +break-cases = fit-or-vertical +doc-comments = before +exp-grouping = preserve +parens-tuple = always +parens-tuple-patterns = always From 79f6f2b763ce2831b82909d14b849bc494c9b600 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 3 Jul 2024 10:31:39 +0200 Subject: [PATCH 03/10] Format the world --- compiler/AssociatedTypes.ml | 15 +++-- compiler/Assumed.ml | 5 +- compiler/Config.ml | 8 ++- compiler/Contexts.ml | 16 +++-- compiler/Cps.ml | 8 ++- compiler/Errors.ml | 9 ++- compiler/Extract.ml | 50 ++++++++++---- compiler/ExtractBase.ml | 41 ++++++++---- compiler/ExtractBuiltin.ml | 17 +++-- compiler/ExtractName.ml | 4 +- compiler/ExtractTypes.ml | 33 ++++++++-- compiler/FunsAnalysis.ml | 9 ++- compiler/Interpreter.ml | 8 ++- compiler/InterpreterBorrows.ml | 53 ++++++++++----- compiler/InterpreterBorrowsCore.ml | 69 +++++++++++--------- compiler/InterpreterExpansion.ml | 10 ++- compiler/InterpreterExpressions.ml | 32 +++++++-- compiler/InterpreterLoopsCore.ml | 6 +- compiler/InterpreterLoopsFixedPoint.ml | 12 +++- compiler/InterpreterLoopsJoinCtxs.ml | 4 +- compiler/InterpreterLoopsMatchCtxs.ml | 4 +- compiler/InterpreterStatements.ml | 33 +++++++--- compiler/InterpreterUtils.ml | 4 +- compiler/Invariants.ml | 7 +- compiler/LlbcAstUtils.ml | 4 +- compiler/PrePasses.ml | 15 +++-- compiler/PrintPure.ml | 6 +- compiler/PureMicroPasses.ml | 22 ++++--- compiler/PureUtils.ml | 65 ++++++++++++------ compiler/ReorderDecls.ml | 3 +- compiler/SymbolicToPure.ml | 24 +++++-- compiler/SynthesizeSymbolic.ml | 3 +- compiler/TypesAnalysis.ml | 4 +- compiler/TypesUtils.ml | 8 ++- compiler/ValuesUtils.ml | 13 +++- tests/src/mutually-recursive-traits.lean.out | 2 +- tests/test_runner/Input.ml | 2 +- tests/test_runner/Utils.ml | 6 +- tests/test_runner/run_test.ml | 6 +- 39 files changed, 454 insertions(+), 186 deletions(-) diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 558cfacf..90a1714f 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -94,9 +94,14 @@ let ctx_add_norm_trait_types_from_preds (span : Meta.span) (ctx : eval_ctx) let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool = match id with | Self | Clause _ -> true - | TraitImpl _ | BuiltinOrAuto _ | TraitRef _ | UnknownTrait _ | FnPointer _ - | Closure _ | Unsolved _ | Dyn _ -> - false + | TraitImpl _ + | BuiltinOrAuto _ + | TraitRef _ + | UnknownTrait _ + | FnPointer _ + | Closure _ + | Unsolved _ + | Dyn _ -> false | ParentClause (id, _, _) | ItemClause (id, _, _, _) -> trait_instance_id_is_local_clause id @@ -293,7 +298,9 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = in let tr : trait_type_ref = { trait_ref; type_name } in (* Lookup the representative, if there is *) - match norm_ctx_get_ty_repr ctx tr with None -> ty | Some ty -> ty) + match norm_ctx_get_ty_repr ctx tr with + | None -> ty + | Some ty -> ty) | TDynTrait _ -> craise_opt_span __FILE__ __LINE__ ctx.span "Dynamic trait types are not supported yet" diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 1720b132..d1f6da94 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -139,7 +139,10 @@ module Sig = struct ] in let inputs = - List.append inputs (match index_ty with None -> [] | Some ty -> [ ty ]) + List.append inputs + (match index_ty with + | None -> [] + | Some ty -> [ ty ]) in let output = mk_ref_ty rvar_0 diff --git a/compiler/Config.ml b/compiler/Config.ml index 98a5eea1..2a32af67 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -41,7 +41,9 @@ let borrow_check = ref false let backend () : backend = Option.get !opt_backend let if_backend (f : unit -> 'a) (default : 'a) : 'a = - match !opt_backend with None -> default | Some _ -> f () + match !opt_backend with + | None -> default + | Some _ -> f () (** {1 Interpreter} *) @@ -374,7 +376,9 @@ let variant_concatenate_type_name = ref true let use_tuple_structs = ref true let backend_has_tuple_projectors backend = - match backend with Lean -> true | Coq | FStar | HOL4 -> false + match backend with + | Lean -> true + | Coq | FStar | HOL4 -> false (** Toggle the use of tuple projectors *) let use_tuple_projectors = ref false diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index 745c22b6..6905676b 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -570,7 +570,9 @@ let ctx_set_abs_can_end (span : Meta.span) (ctx : eval_ctx) let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool = let decl_group = TypeDeclId.Map.find id ctx.type_ctx.type_decls_groups in - match decl_group with RecGroup _ -> true | NonRecGroup _ -> false + match decl_group with + | RecGroup _ -> true + | NonRecGroup _ -> false (** Visitor to iterate over the values in the *current* frame *) class ['self] iter_frame = @@ -626,17 +628,23 @@ class ['self] map_eval_ctx = let env_iter_abs (f : abs -> unit) (env : env) : unit = List.iter (fun (ee : env_elem) -> - match ee with EBinding _ | EFrame -> () | EAbs abs -> f abs) + match ee with + | EBinding _ | EFrame -> () + | EAbs abs -> f abs) env let env_map_abs (f : abs -> abs) (env : env) : env = List.map (fun (ee : env_elem) -> - match ee with EBinding _ | EFrame -> ee | EAbs abs -> EAbs (f abs)) + match ee with + | EBinding _ | EFrame -> ee + | EAbs abs -> EAbs (f abs)) env let env_filter_abs (f : abs -> bool) (env : env) : env = List.filter (fun (ee : env_elem) -> - match ee with EBinding _ | EFrame -> true | EAbs abs -> f abs) + match ee with + | EBinding _ | EFrame -> true + | EAbs abs -> f abs) env diff --git a/compiler/Cps.ml b/compiler/Cps.ml index 917989ff..e77db88e 100644 --- a/compiler/Cps.ml +++ b/compiler/Cps.ml @@ -92,10 +92,14 @@ let map_apply_continuation (f : 'a -> 'c -> 'b * 'c * ('e -> 'e)) eval_list inputs ctx let cc_singleton file line span cf el = - match el with [ e ] -> cf e | _ -> internal_error file line span + match el with + | [ e ] -> cf e + | _ -> internal_error file line span let cf_singleton file line span el = - match el with [ e ] -> e | _ -> internal_error file line span + match el with + | [ e ] -> e + | _ -> internal_error file line span (** It happens that we need to concatenate lists of results, for instance when evaluating the branches of a match. When applying diff --git a/compiler/Errors.ml b/compiler/Errors.ml index 838e1e37..29f70dfa 100644 --- a/compiler/Errors.ml +++ b/compiler/Errors.ml @@ -1,7 +1,10 @@ let log = Logging.errors_log let raw_span_to_string (raw_span : Meta.raw_span) = - let file = match raw_span.file with Virtual s | Local s -> s in + let file = + match raw_span.file with + | Virtual s | Local s -> s + in let loc_to_string (l : Meta.loc) : string = string_of_int l.line ^ ":" ^ string_of_int l.col in @@ -14,7 +17,9 @@ let span_to_string (span : Meta.span) = raw_span_to_string span.span let format_error_message (span : Meta.span option) (msg : string) = let span = - match span with None -> "" | Some span -> "\n" ^ span_to_string span + match span with + | None -> "" + | Some span -> "\n" ^ span_to_string span in msg ^ span diff --git a/compiler/Extract.ml b/compiler/Extract.ml index c1c4eeea..c771fff0 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -586,7 +586,9 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx) | _ -> None in let has_one_field = - match num_fields with Some len -> len = 1 | None -> false + match num_fields with + | Some len -> len = 1 + | None -> false in if is_tuple_struct && has_one_field then extract_texpression span ctx fmt inside arg @@ -924,7 +926,9 @@ 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] *) @@ -943,7 +947,9 @@ 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 *) @@ -1049,10 +1055,14 @@ 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 () -> @@ -1100,7 +1110,9 @@ 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; @@ -1599,7 +1611,11 @@ 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 (); @@ -1833,7 +1849,11 @@ 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 (); @@ -2310,7 +2330,9 @@ let extract_trait_item (ctx : extraction_ctx) (fmt : F.formatter) (* ":" or "=" *) F.pp_print_string fmt separator; ty (); - (match 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) @@ -2319,7 +2341,11 @@ 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 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 *) @@ -2366,7 +2392,9 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter) f.signature.llbc_generics 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 diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 4d05f0d0..52a163eb 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -389,14 +389,18 @@ type names_maps = { (** Return [true] if we are strict on collisions for this id (i.e., we forbid collisions even with the ids in the unsafe names map) *) let strict_collisions (id : id) : bool = - match id with UnknownId | TypeId _ -> true | _ -> false + match id with + | UnknownId | TypeId _ -> true + | _ -> false (** We might not check for collisions for some specific ids (ex.: field names) *) let allow_collisions (id : id) : bool = match id with - | FieldId _ | TraitItemClauseId _ | TraitParentClauseId _ | TraitItemId _ - | TraitMethodId _ -> - !Config.record_fields_short_names + | FieldId _ + | TraitItemClauseId _ + | TraitParentClauseId _ + | TraitItemId _ + | TraitMethodId _ -> !Config.record_fields_short_names | FunId (Pure _ | FromLlbc (FunId (FAssumed _), _)) -> (* We map several assumed functions to the same id *) true @@ -534,9 +538,13 @@ 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. @@ -801,7 +809,9 @@ let unop_name (unop : unop) : string = | 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") @@ -1676,7 +1686,9 @@ 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 = @@ -1685,7 +1697,9 @@ 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 = @@ -1826,7 +1840,10 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx) | FStar -> "x" (* lacking inspiration here... *) | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *)) | TLiteral lty -> ( - match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i") + match lty with + | TBool -> "b" + | TChar -> "c" + | TInteger _ -> "i") | TArrow _ -> "f" | TTraitType (_, name) -> name_from_type_ident name | Error -> "x") @@ -2055,7 +2072,9 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : between the name for the default constant and the name for the field in the trait declaration *) let suffix = - match def.kind with TraitItemProvided _ -> "_default" | _ -> "" + match def.kind with + | TraitItemProvided _ -> "_default" + | _ -> "" in let ctx = ctx_add def.item_meta.span decl (name ^ suffix) ctx in let ctx = ctx_add def.item_meta.span body (name ^ suffix ^ "_body") ctx in diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 37b676bb..71565399 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -49,7 +49,9 @@ let flatten_name (name : string list) : string = (** 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 +63,9 @@ 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,10 +139,15 @@ 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" + match backend () with + | FStar | Coq | HOL4 -> "" + | Lean -> ".mk" in prefix ^ type_name ^ suffix diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml index 81c35847..32901248 100644 --- a/compiler/ExtractName.ml +++ b/compiler/ExtractName.ml @@ -37,7 +37,9 @@ let pattern_to_extract_name (span : Meta.span option) (name : pattern) : let c = { tgt = TkName } in let all_vars = let check (g : generic_arg) : bool = - match g with GExpr (EVar _) | GRegion (RVar _) -> true | _ -> false + match g with + | GExpr (EVar _) | GRegion (RVar _) -> true + | _ -> false in List.for_all check in diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 78382179..6b196548 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -240,7 +240,11 @@ let extract_binop (span : Meta.span) F.pp_print_space fmt (); extract_expr false arg1 | _ -> - let binop_is_shift = match binop with Shl | Shr -> true | _ -> false in + let binop_is_shift = + match binop with + | Shl | Shr -> true + | _ -> false + in let binop = named_binop_name binop int_ty in F.pp_print_string fmt binop; (* In the case of F*, for shift operations, because machine integers @@ -258,15 +262,21 @@ let extract_binop (span : Meta.span) if inside then F.pp_print_string fmt ")" let is_single_opaque_fun_decl_group (dg : Pure.fun_decl list) : bool = - match dg with [ d ] -> d.body = None | _ -> false + match dg with + | [ d ] -> d.body = None + | _ -> false let is_single_opaque_type_decl_group (dg : Pure.type_decl list) : bool = - match dg with [ d ] -> d.kind = Opaque | _ -> false + match dg with + | [ d ] -> d.kind = Opaque + | _ -> false let is_empty_record_type_decl (d : Pure.type_decl) : bool = d.kind = Struct [] let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool = - match dg with [ d ] -> is_empty_record_type_decl d | _ -> false + match dg with + | [ d ] -> is_empty_record_type_decl d + | _ -> false (** In some provers, groups of definitions must be delimited. @@ -402,7 +412,9 @@ 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 = @@ -993,7 +1005,11 @@ 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 (); @@ -1392,7 +1408,10 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) in let is_tuple_struct_one_or_zero_field = is_tuple_struct - && match def.kind with Struct [] | Struct [ _ ] -> true | _ -> false + && + match def.kind with + | Struct [] | Struct [ _ ] -> true + | _ -> false in let type_kind = if extract_body then diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index d448c173..859bc116 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -104,8 +104,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) method! visit_rvalue _env rv = match rv with | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ | Len _ - -> - () + -> () | UnaryOp (uop, _) -> can_fail := unop_can_fail uop || !can_fail | BinaryOp (bop, _, _) -> can_fail := binop_can_fail bop || !can_fail @@ -202,7 +201,11 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let analyze_fun_decl_group (d : fun_declaration_group) : unit = (* Retrieve the function declarations *) - let funs = match d with NonRecGroup id -> [ id ] | RecGroup ids -> ids in + let funs = + match d with + | NonRecGroup id -> [ id ] + | RecGroup ids -> ids + in let funs = List.map (fun id -> FunDeclId.Map.find id funs_map) funs in let fun_ids = List.map (fun (d : fun_decl) -> d.def_id) funs in let fun_ids = FunDeclId.Set.of_list fun_ids in diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index afa189e3..3d665de6 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -391,7 +391,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) | Loop (_, rg_id', kind) -> let rg_id' = Option.get rg_id' in let is_ret = - match kind with LoopSynthInput -> true | LoopCall -> false + match kind with + | LoopSynthInput -> true + | LoopCall -> false in rg_id' = back_id && is_ret | _ -> false @@ -491,7 +493,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) in let current_abs_id = - match current_abs_id with None -> [] | Some id -> [ id ] + match current_abs_id with + | None -> [] + | Some id -> [ id ] in let target_abs_ids = List.append parent_input_abs_ids current_abs_id in let ctx, cc = diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index f3d2396a..f67be365 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -836,9 +836,10 @@ let give_back (config : config) (span : Meta.span) (l : BorrowId.id) (* Update the context *) give_back_shared config span l ctx | Abstract - ( AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ - | AEndedSharedBorrow ) -> - craise __FILE__ __LINE__ span "Unreachable" + ( AEndedMutBorrow _ + | AIgnoredMutBorrow _ + | AEndedIgnoredMutBorrow _ + | AEndedSharedBorrow ) -> craise __FILE__ __LINE__ span "Unreachable" let check_borrow_disappeared (span : Meta.span) (fun_name : string) (l : BorrowId.id) (ctx0 : eval_ctx) (ctx : eval_ctx) : unit = @@ -1181,11 +1182,16 @@ and end_abstraction_borrows (config : config) (span : Meta.span) (* Raise an exception only if the asb contains borrows *) if List.exists - (fun x -> match x with AsbBorrow _ -> true | _ -> false) + (fun x -> + match x with + | AsbBorrow _ -> true + | _ -> false) asb then raise (FoundABorrowContent bc) else () - | AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ + | AEndedMutBorrow _ + | AIgnoredMutBorrow _ + | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow -> (* Nothing to do for ignored borrows *) () @@ -1261,9 +1267,10 @@ and end_abstraction_borrows (config : config) (span : Meta.span) in (* Continue *) ctx - | AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ - | AEndedSharedBorrow -> - craise __FILE__ __LINE__ span "Unexpected" + | AEndedMutBorrow _ + | AIgnoredMutBorrow _ + | AEndedIgnoredMutBorrow _ + | AEndedSharedBorrow -> craise __FILE__ __LINE__ span "Unexpected" in (* Reexplore *) end_abstraction_borrows config span chain abs_id ctx @@ -2093,8 +2100,11 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) (match lc with | ASharedLoan (pm, bids, _, _) -> push_loans pm bids (Abstract (ty, lc)) | AMutLoan (pm, bid, _) -> push_loan pm bid (Abstract (ty, lc)) - | AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _ - | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ -> + | AEndedMutLoan _ + | AEndedSharedLoan _ + | AIgnoredMutLoan _ + | AEndedIgnoredMutLoan _ + | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) craise __FILE__ __LINE__ span "Unreachable"); (* Continue *) @@ -2120,7 +2130,9 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) craise __FILE__ __LINE__ span "Unreachable" in List.iter register asb - | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedMutBorrow _ + | AIgnoredMutBorrow _ + | AEndedIgnoredMutBorrow _ + | AEndedMutBorrow _ | AEndedSharedBorrow -> (* The abstraction has been destructured, so those shouldn't appear *) craise __FILE__ __LINE__ span "Unreachable"); @@ -2345,12 +2357,14 @@ let merge_abstractions_merge_loan_borrow_pairs (span : Meta.span) if merge_funs = None then ( sanity_check __FILE__ __LINE__ (List.for_all - (function LoanId (pm, _) | BorrowId (pm, _) -> pm = PNone) + (function + | LoanId (pm, _) | BorrowId (pm, _) -> pm = PNone) borrows_loans0) span; sanity_check __FILE__ __LINE__ (List.for_all - (function LoanId (pm, _) | BorrowId (pm, _) -> pm = PNone) + (function + | LoanId (pm, _) | BorrowId (pm, _) -> pm = PNone) borrows_loans1) span; sanity_check __FILE__ __LINE__ @@ -2391,7 +2405,9 @@ let merge_abstractions_merge_loan_borrow_pairs (span : Meta.span) avalues := av :: !avalues in let push_opt_avalue av = - match av with None -> () | Some av -> push_avalue av + match av with + | None -> () + | Some av -> push_avalue av in (* Compute the intersection of: @@ -2529,8 +2545,10 @@ let merge_abstractions_merge_loan_borrow_pairs (span : Meta.span) | AMutLoan _ -> set_loan_as_merged bid; Some { value = ALoan lc; ty } - | AEndedMutLoan _ | AEndedSharedLoan _ - | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _ + | AEndedMutLoan _ + | AEndedSharedLoan _ + | AIgnoredMutLoan _ + | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) craise __FILE__ __LINE__ span "Unreachable")) @@ -3039,7 +3057,8 @@ let reorder_fresh_abs_aux (span : Meta.span) (old_abs_ids : AbstractionId.Set.t) let env, fresh_abs = List.partition (function - | EAbs abs -> AbstractionId.Set.mem abs.abs_id old_abs_ids | _ -> true) + | EAbs abs -> AbstractionId.Set.mem abs.abs_id old_abs_ids + | _ -> true) ctx.env in diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 0469d58e..b0ace136 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -48,7 +48,10 @@ type priority_borrows_or_abs = | InnerLoans of borrow_ids [@@deriving show] -let update_if_none opt x = match opt with None -> Some x | _ -> opt +let update_if_none opt x = + match opt with + | None -> Some x + | _ -> opt (** Utility exception *) exception FoundPriority of priority_borrows_or_abs @@ -271,8 +274,7 @@ let lookup_loan_opt (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) | AIgnoredMutLoan (_, _) | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_span = _ } - | AIgnoredSharedLoan _ -> - super#visit_aloan_content env lc + | AIgnoredSharedLoan _ -> super#visit_aloan_content env lc method! visit_EBinding env bv v = sanity_check __FILE__ __LINE__ (Option.is_none !abs_or_var) span; @@ -414,8 +416,7 @@ let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) | AIgnoredMutLoan (_, _) | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_span = _ } - | AIgnoredSharedLoan _ -> - super#visit_aloan_content env lc + | AIgnoredSharedLoan _ -> super#visit_aloan_content env lc (** Note that once inside the abstractions, we don't control diving (there are no use cases requiring finer control). *) @@ -475,8 +476,7 @@ let lookup_borrow_opt (span : Meta.span) (ek : exploration_kind) | AEndedMutBorrow _ | AEndedIgnoredMutBorrow { given_back = _; child = _; given_back_span = _ } - | AEndedSharedBorrow -> - super#visit_aborrow_content env bc + | AEndedSharedBorrow -> super#visit_aborrow_content env bc | AProjSharedBorrow asb -> if borrow_in_asb l asb then raise (FoundGBorrowContent (Abstract bc)) @@ -593,9 +593,10 @@ let update_aborrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) sanity_check __FILE__ __LINE__ (pm = PNone) span; if bid = l then update () else ABorrow (super#visit_ASharedBorrow env pm bid) - | AIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedSharedBorrow - | AEndedIgnoredMutBorrow _ -> - super#visit_ABorrow env bc + | AIgnoredMutBorrow _ + | AEndedMutBorrow _ + | AEndedSharedBorrow + | AEndedIgnoredMutBorrow _ -> super#visit_ABorrow env bc | AProjSharedBorrow asb -> if borrow_in_asb l asb then update () else ABorrow (super#visit_AProjSharedBorrow env asb) @@ -767,9 +768,10 @@ let lookup_intersecting_aproj_borrows_opt (span : Meta.span) method! visit_aproj abs sproj = (let abs = Option.get abs in match sproj with - | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows _ - | AIgnoredProjBorrows -> - () + | AProjLoans _ + | AEndedProjLoans _ + | AEndedProjBorrows _ + | AIgnoredProjBorrows -> () | AProjBorrows (sv', proj_rty) -> let is_shared = false in check_add_proj_borrows is_shared abs sv' proj_rty); @@ -865,9 +867,10 @@ let update_intersecting_aproj_borrows (span : Meta.span) method! visit_aproj abs sproj = match sproj with - | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows _ - | AIgnoredProjBorrows -> - super#visit_aproj abs sproj + | AProjLoans _ + | AEndedProjLoans _ + | AEndedProjBorrows _ + | AIgnoredProjBorrows -> super#visit_aproj abs sproj | AProjBorrows (sv', proj_rty) -> let abs = Option.get abs in let is_shared = true in @@ -981,9 +984,10 @@ let update_intersecting_aproj_loans (span : Meta.span) method! visit_aproj abs sproj = match sproj with - | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _ - | AIgnoredProjBorrows -> - super#visit_aproj abs sproj + | AProjBorrows _ + | AEndedProjLoans _ + | AEndedProjBorrows _ + | AIgnoredProjBorrows -> super#visit_aproj abs sproj | AProjLoans (sv', given_back) -> let abs = Option.get abs in if same_symbolic_id sv sv' then ( @@ -1032,9 +1036,10 @@ let lookup_aproj_loans (span : Meta.span) (abs_id : AbstractionId.id) method! visit_aproj (abs : abs option) sproj = (match sproj with - | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _ - | AIgnoredProjBorrows -> - super#visit_aproj abs sproj + | AProjBorrows _ + | AEndedProjLoans _ + | AEndedProjBorrows _ + | AIgnoredProjBorrows -> super#visit_aproj abs sproj | AProjLoans (sv', given_back) -> let abs = Option.get abs in sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) span; @@ -1078,9 +1083,10 @@ let update_aproj_loans (span : Meta.span) (abs_id : AbstractionId.id) method! visit_aproj (abs : abs option) sproj = match sproj with - | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _ - | AIgnoredProjBorrows -> - super#visit_aproj abs sproj + | AProjBorrows _ + | AEndedProjLoans _ + | AEndedProjBorrows _ + | AIgnoredProjBorrows -> super#visit_aproj abs sproj | AProjLoans (sv', _) -> let abs = Option.get abs in sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) span; @@ -1127,9 +1133,10 @@ let update_aproj_borrows (span : Meta.span) (abs_id : AbstractionId.id) method! visit_aproj (abs : abs option) sproj = match sproj with - | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows _ - | AIgnoredProjBorrows -> - super#visit_aproj abs sproj + | AProjLoans _ + | AEndedProjLoans _ + | AEndedProjBorrows _ + | AIgnoredProjBorrows -> super#visit_aproj abs sproj | AProjBorrows (sv', _proj_ty) -> let abs = Option.get abs in sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) span; @@ -1207,8 +1214,7 @@ let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) : sanity_check __FILE__ __LINE__ (pm = PNone) span; raise (FoundBorrowIds (Borrows bids)) | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } - | AEndedSharedLoan (_, _) -> - super#visit_aloan_content env lc + | AEndedSharedLoan (_, _) -> super#visit_aloan_content env lc | AIgnoredMutLoan (_, _) -> (* Ignore *) super#visit_aloan_content env lc @@ -1230,8 +1236,7 @@ let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) : method! visit_aproj env sproj = (match sproj with | AProjBorrows (_, _) - | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> - () + | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> () | AProjLoans (sv, _) -> raise (ValuesUtils.FoundSymbolicValue sv)); super#visit_aproj env sproj end diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index b14331fd..a17e308c 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -665,9 +665,13 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) : (* We can't expand those *) craise __FILE__ __LINE__ span "Attempted to greedily expand an ADT which can't be expanded " - | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ - | TDynTrait _ -> - craise __FILE__ __LINE__ span "Unreachable" + | TVar _ + | TLiteral _ + | TNever + | TTraitType _ + | TArrow _ + | TRawPtr _ + | TDynTrait _ -> craise __FILE__ __LINE__ span "Unreachable" in (* *) log#ldebug diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 5088d29a..1aae859f 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -536,9 +536,21 @@ let eval_binary_op_concrete_compute (span : Meta.span) (binop : binop) | Le -> Z.leq sv1.value sv2.value | Ge -> Z.geq sv1.value sv2.value | Gt -> Z.gt sv1.value sv2.value - | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr | Shl - | Shr | Ne | Eq | CheckedAdd | CheckedSub | CheckedMul -> - craise __FILE__ __LINE__ span "Unreachable" + | Div + | Rem + | Add + | Sub + | Mul + | BitXor + | BitAnd + | BitOr + | Shl + | Shr + | Ne + | Eq + | CheckedAdd + | CheckedSub + | CheckedMul -> craise __FILE__ __LINE__ span "Unreachable" in Ok ({ value = VLiteral (VBool b); ty = TLiteral TBool } @@ -561,9 +573,17 @@ let eval_binary_op_concrete_compute (span : Meta.span) (binop : binop) | BitXor -> raise Unimplemented | BitAnd -> raise Unimplemented | BitOr -> raise Unimplemented - | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq | CheckedAdd - | CheckedSub | CheckedMul -> - craise __FILE__ __LINE__ span "Unreachable" + | Lt + | Le + | Ge + | Gt + | Shl + | Shr + | Ne + | Eq + | CheckedAdd + | CheckedSub + | CheckedMul -> craise __FILE__ __LINE__ span "Unreachable" in match res with | Error _ -> Error EPanic diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index df808385..2502e700 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -392,7 +392,11 @@ let ctx_split_fixed_new (span : Meta.span) (fixed_ids : ids_sets) | EAbs abs -> is_fresh_abs_id abs.abs_id in let new_eel, filt_env = List.partition is_fresh ctx.env in - let is_abs ee = match ee with EAbs _ -> true | _ -> false in + let is_abs ee = + match ee with + | EAbs _ -> true + | _ -> false + in let new_absl, new_dummyl = List.partition is_abs new_eel in let new_absl = List.map diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index e1a5c428..3b339ef8 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -135,7 +135,9 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : *) let absl = List.filter_map - (function EBinding _ | EFrame -> None | EAbs abs -> Some abs) + (function + | EBinding _ | EFrame -> None + | EAbs abs -> Some abs) ctx.env in let absl_ids, absl_id_maps = compute_absl_ids absl in @@ -352,7 +354,9 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : let env = let bmap = BorrowId.Map.of_list !borrow_substs in let bsusbt bid = - match BorrowId.Map.find_opt bid bmap with None -> bid | Some bid -> bid + match BorrowId.Map.find_opt bid bmap with + | None -> bid + | Some bid -> bid in let visitor = @@ -700,7 +704,9 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) we will explore them in this order) *) let all_abs_ids = List.filter_map - (function EAbs abs -> Some abs.abs_id | _ -> None) + (function + | EAbs abs -> Some abs.abs_id + | _ -> None) (* TODO: we may want to use a different order, for instance the order in which the regions were ended. *) (List.rev !fp.env) diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 9ca332b2..4f89b22f 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -482,7 +482,9 @@ let eval_ctx_has_markers (ctx : eval_ctx) : bool = inherit [_] iter_eval_ctx method! visit_proj_marker _ pm = - match pm with PNone -> () | PLeft | PRight -> raise Found + match pm with + | PNone -> () + | PLeft | PRight -> raise Found end in try diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index d6be0856..60429d8e 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -1566,7 +1566,9 @@ let prepare_match_ctx_with_target (config : config) (span : Meta.span) (* Remove the abstractions *) let filter (ee : env_elem) : bool = - match ee with EBinding _ -> true | EAbs _ | EFrame -> false + match ee with + | EBinding _ -> true + | EAbs _ | EFrame -> false in let filt_src_env = List.filter filter filt_src_env in let filt_tgt_env = List.filter filter filt_tgt_env in diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 67ac15d9..cf104d77 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -537,10 +537,13 @@ let eval_assumed_function_call_concrete (config : config) (span : Meta.span) | BoxFree -> (* Should have been treated above *) craise __FILE__ __LINE__ span "Unreachable" - | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared - | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut - -> - craise __FILE__ __LINE__ span "Unimplemented" + | ArrayIndexShared + | ArrayIndexMut + | ArrayToSliceShared + | ArrayToSliceMut + | ArrayRepeat + | SliceIndexShared + | SliceIndexMut -> craise __FILE__ __LINE__ span "Unimplemented" in let cc = cc_comp cc cf_eval_body in @@ -865,7 +868,9 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span) let provided = List.filter_map (fun (id, f) -> - match f with None -> None | Some f -> Some (id, f)) + match f with + | None -> None + | Some f -> Some (id, f)) trait_decl.provided_methods in List.find @@ -1009,8 +1014,13 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun = (* Evaluation successful: evaluate the second statement *) | Unit -> eval_statement config st2 ctx (* Control-flow break: transmit. We enumerate the cases on purpose *) - | Panic | Break _ | Continue _ | Return | LoopReturn _ - | EndEnterLoop _ | EndContinue _ -> + | Panic + | Break _ + | Continue _ + | Return + | LoopReturn _ + | EndEnterLoop _ + | EndContinue _ -> ([ (ctx, res) ], cf_singleton __FILE__ __LINE__ st.span)) ctx_resl in @@ -1336,9 +1346,12 @@ and eval_transparent_function_call_concrete (config : config) (span : Meta.span) its destination and continue *) let ctx, cf = pop_frame_assign config span dest ctx in ((ctx, Unit), cf) - | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ - | EndContinue _ -> - craise __FILE__ __LINE__ span "Unreachable") + | Break _ + | Continue _ + | Unit + | LoopReturn _ + | EndEnterLoop _ + | EndContinue _ -> craise __FILE__ __LINE__ span "Unreachable") ctx_resl in let ctx_resl, cfl = List.split ctx_resl_cfl in diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index f3f12906..f577153f 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -129,7 +129,9 @@ let mk_aproj_borrows_from_symbolic_value (span : Meta.span) (** TODO: move *) let borrow_is_asb (bid : BorrowId.id) (asb : abstract_shared_borrow) : bool = - match asb with AsbBorrow bid' -> bid' = bid | AsbProjReborrows _ -> false + match asb with + | AsbBorrow bid' -> bid' = bid + | AsbProjReborrows _ -> false (** TODO: move *) let borrow_in_asb (bid : BorrowId.id) (asb : abstract_shared_borrows) : bool = diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 50e6e87f..2a7f0bd0 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -250,7 +250,9 @@ let check_loans_borrows_relation_invariant (span : Meta.span) (ctx : eval_ctx) : | ASharedBorrow (_, bid) -> register_borrow BShared bid | AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow RMut bid | AIgnoredMutBorrow (None, _) - | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow + | AEndedMutBorrow _ + | AEndedIgnoredMutBorrow _ + | AEndedSharedBorrow | AProjSharedBorrow _ -> (* Do nothing *) () @@ -362,8 +364,7 @@ let check_borrowed_values_invariant (span : Meta.span) (ctx : eval_ctx) : unit = | AMutBorrow (_, _, _) -> set_outer_mut info | ASharedBorrow _ | AEndedSharedBorrow -> set_outer_shared info | AIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _ - -> - set_outer_mut info + -> set_outer_mut info | AProjSharedBorrow _ -> set_outer_shared info in (* Continue exploring *) diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index e7b85c30..e10e316c 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -44,7 +44,9 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : d.body = None (* Something to pay attention to: we must ignore trait method *declarations* (which don't have a body but must not be considered as opaque) *) - && (match d.kind with TraitItemDecl _ -> false | _ -> true) + && (match d.kind with + | TraitItemDecl _ -> false + | _ -> true) && ((not filter_assumed) || (not (NameMatcherMap.mem ctx d.item_meta.name builtin_globals_map)) && not (NameMatcherMap.mem ctx d.item_meta.name (builtin_funs_map ())) diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml index 6bdf0a01..f16fba86 100644 --- a/compiler/PrePasses.ml +++ b/compiler/PrePasses.ml @@ -99,9 +99,14 @@ let remove_useless_cf_merges (crate : crate) (f : fun_decl) : fun_decl = * *) let rec can_be_moved_aux (must_end_with_exit : bool) (st : statement) : bool = match st.content with - | SetDiscriminant _ | Assert _ | Call _ | Break _ | Continue _ | Switch _ - | Loop _ | Error _ -> - false + | SetDiscriminant _ + | Assert _ + | Call _ + | Break _ + | Continue _ + | Switch _ + | Loop _ + | Error _ -> false | Assign (_, rv) -> ( match rv with | Use _ | RvRef _ -> not must_end_with_exit @@ -438,7 +443,9 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl = (* Remove the type aliases from the type declarations and declaration groups *) let filter_type_aliases (crate : crate) : crate = let type_decl_is_alias (ty : type_decl) = - match ty.kind with Alias _ -> true | _ -> false + match ty.kind with + | Alias _ -> true + | _ -> false in (* Whether the declaration group has a single entry that is a type alias. Type aliases should not be in recursive groups so we also ensure this doesn't diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 413f7f0d..a142aa8f 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -284,7 +284,11 @@ let rec mprojection_to_string (env : fmt_env) (inside : string) "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name)) let mplace_to_string (env : fmt_env) (p : mplace) : string = - let name = match p.name with None -> "" | Some name -> name in + let name = + match p.name with + | None -> "" + | Some name -> name + in (* We add the "llbc" suffix to the variable index, because span-places * use indices of the variables in the original LLBC program, while * regular places use indices for the pure variables: we want to make diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 3476df5f..896376bc 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -306,7 +306,9 @@ let compute_pretty_names (def : fun_decl) : fun_decl = (* Register the place *) let ctx = register_mplace mp ctx in (* Add the constraint *) - match (unspan rv).e with Var vid -> add_constraint mp vid ctx | _ -> ctx + match (unspan rv).e with + | Var vid -> add_constraint mp vid ctx + | _ -> ctx in let add_pure_var_value_constraint (var_id : VarId.id) (rv : texpression) (ctx : pn_ctx) : pn_ctx = @@ -331,7 +333,9 @@ let compute_pretty_names (def : fun_decl) : fun_decl = (* Register the variable *) let ctx = register_var (self#zero ()) v in (* Register the mplace information if there is such information *) - match mp with Some mp -> add_constraint mp v.id ctx | None -> ctx + match mp with + | Some mp -> add_constraint mp v.id ctx + | None -> ctx end in let ctx1 = obj#visit_typed_pattern () lv () in @@ -1008,8 +1012,7 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl = | Var _ | CVar _ | Const _ | App _ | Qualif _ | Meta (_, _) | StructUpdate _ | Lambda _ - | EError (_, _) -> - super#visit_expression env e + | EError (_, _) -> super#visit_expression env e | Switch (scrut, switch) -> ( match switch with | If (_, _) -> super#visit_expression env e @@ -1588,10 +1591,13 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = sanity_check __FILE__ __LINE__ (args = []) def.item_meta.span; mk_unit_rvalue - | SliceIndexShared | SliceIndexMut | ArrayIndexShared - | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut - | ArrayRepeat -> - super#visit_texpression env e) + | SliceIndexShared + | SliceIndexMut + | ArrayIndexShared + | ArrayIndexMut + | ArrayToSliceShared + | ArrayToSliceMut + | ArrayRepeat -> super#visit_texpression env e) | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e end diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 9673f542..579b3dd5 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -76,7 +76,9 @@ let fun_sig_info_is_wf (info : fun_sig_info) : bool = inputs_info_is_wf info.fwd_info let opt_dest_arrow_ty (ty : ty) : (ty * ty) option = - match ty with TArrow (arg_ty, ret_ty) -> Some (arg_ty, ret_ty) | _ -> None + match ty with + | TArrow (arg_ty, ret_ty) -> Some (arg_ty, ret_ty) + | _ -> None let is_arrow_ty (ty : ty) : bool = Option.is_some (opt_dest_arrow_ty ty) @@ -181,7 +183,9 @@ let type_decl_get_fields (def : type_decl) | Struct fields, None -> fields | _ -> let opt_variant_id = - match opt_variant_id with None -> "None" | Some _ -> "Some" + match opt_variant_id with + | None -> "None" + | Some _ -> "Some" in raise (Invalid_argument @@ -246,19 +250,29 @@ let texpression_requires_parentheses span e = | Coq | HOL4 -> let_group_requires_parentheses span e let is_var (e : texpression) : bool = - match e.e with Var _ -> true | _ -> false + match e.e with + | Var _ -> true + | _ -> false let as_var (span : Meta.span) (e : texpression) : VarId.id = - match e.e with Var v -> v | _ -> craise __FILE__ __LINE__ span "Not a var" + match e.e with + | Var v -> v + | _ -> craise __FILE__ __LINE__ span "Not a var" let is_cvar (e : texpression) : bool = - match e.e with CVar _ -> true | _ -> false + match e.e with + | CVar _ -> true + | _ -> false let is_global (e : texpression) : bool = - match e.e with Qualif { id = Global _; _ } -> true | _ -> false + match e.e with + | Qualif { id = Global _; _ } -> true + | _ -> false let is_const (e : texpression) : bool = - match e.e with Const _ -> true | _ -> false + match e.e with + | Const _ -> true + | _ -> false let ty_as_adt (span : Meta.span) (ty : ty) : type_id * generic_args = match ty with @@ -267,7 +281,9 @@ let ty_as_adt (span : Meta.span) (ty : ty) : type_id * generic_args = (** Remove the external occurrences of {!Meta} *) let rec unspan (e : texpression) : texpression = - match e.e with Meta (_, e) -> unspan e | _ -> e + match e.e with + | Meta (_, e) -> unspan e + | _ -> e (** Remove *all* the span information *) let remove_span (e : texpression) : texpression = @@ -284,7 +300,9 @@ let mk_arrow (ty0 : ty) (ty1 : ty) : ty = TArrow (ty0, ty1) (** Construct a type as a list of arrows: ty1 -> ... tyn *) let mk_arrows (inputs : ty list) (output : ty) = let rec aux (tys : ty list) : ty = - match tys with [] -> output | ty :: tys' -> TArrow (ty, aux tys') + match tys with + | [] -> output + | ty :: tys' -> TArrow (ty, aux tys') in aux inputs @@ -328,7 +346,9 @@ let destruct_lets_no_interleave (span : Meta.span) (e : texpression) : let destruct_apps (e : texpression) : texpression * texpression list = let rec aux (args : texpression list) (e : texpression) : texpression * texpression list = - match e.e with App (f, x) -> aux (x :: args) f | _ -> (e, args) + match e.e with + | App (f, x) -> aux (x :: args) f + | _ -> (e, args) in aux [] e @@ -366,7 +386,9 @@ let mk_apps (span : Meta.span) (app : texpression) (args : texpression list) : let opt_destruct_qualif_app (e : texpression) : (qualif * texpression list) option = let app, args = destruct_apps e in - match app.e with Qualif qualif -> Some (qualif, args) | _ -> None + match app.e with + | Qualif qualif -> Some (qualif, args) + | _ -> None (** Destruct an expression into a qualif identifier and a list of arguments *) let destruct_qualif_app (e : texpression) : qualif * texpression list = @@ -501,7 +523,9 @@ let mk_mplace_texpression (mp : mplace) (e : texpression) : texpression = let mk_opt_mplace_texpression (mp : mplace option) (e : texpression) : texpression = - match mp with None -> e | Some mp -> mk_mplace_texpression mp e + match mp with + | None -> e + | Some mp -> mk_mplace_texpression mp e (** Make a "simplified" tuple value from a list of values: - if there is exactly one value, just return it @@ -567,8 +591,7 @@ let unwrap_result_ty (span : Meta.span) (ty : ty) : ty = match ty with | TAdt ( TAssumed TResult, - { types = [ ty ]; const_generics = []; trait_refs = [] } ) -> - ty + { types = [ ty ]; const_generics = []; trait_refs = [] } ) -> ty | _ -> craise __FILE__ __LINE__ span "not a result type" let mk_result_fail_texpression (span : Meta.span) (error : texpression) @@ -622,7 +645,9 @@ let mk_result_ok_pattern (v : typed_pattern) : typed_pattern = { value; ty } let opt_unspan_mplace (e : texpression) : mplace option * texpression = - match e.e with Meta (MPlace mp, e) -> (Some mp, e) | _ -> (None, e) + match e.e with + | Meta (MPlace mp, e) -> (Some mp, e) + | _ -> (None, e) let mk_state_var (id : VarId.id) : var = { id; basename = Some ConstStrings.state_basename; ty = mk_state_ty } @@ -667,7 +692,9 @@ let rec typed_pattern_to_texpression (span : Meta.span) (pat : typed_pattern) : (* Apply the constructor *) Some (mk_apps span cons fields_values).e in - match e_opt with None -> None | Some e -> Some { e; ty = pat.ty } + match e_opt with + | None -> None + | Some e -> Some { e; ty = pat.ty } type trait_decl_method_decl_id = { is_provided : bool; id : fun_decl_id } @@ -765,8 +792,7 @@ let opt_dest_tuple_texpression (e : texpression) : texpression list option = let app, args = destruct_apps e in match app.e with | Qualif { id = AdtCons { adt_id = TTuple; variant_id = None }; generics = _ } - -> - Some args + -> Some args | _ -> None let opt_dest_struct_pattern (pat : typed_pattern) : typed_pattern list option = @@ -788,6 +814,5 @@ let opt_destruct_ret (e : texpression) : texpression option = ty = _; }, arg ) - when variant_id = Some result_ok_id -> - Some arg + when variant_id = Some result_ok_id -> Some arg | _ -> None diff --git a/compiler/ReorderDecls.ml b/compiler/ReorderDecls.ml index f5443e03..748406f2 100644 --- a/compiler/ReorderDecls.ml +++ b/compiler/ReorderDecls.ml @@ -34,8 +34,7 @@ let compute_body_fun_deps (e : texpression) : FunIdSet.t = method! visit_qualif _ id = match id.id with | FunOrOp (Unop _ | Binop _) - | Global _ | AdtCons _ | Proj _ | TraitConst _ -> - () + | Global _ | AdtCons _ | Proj _ | TraitConst _ -> () | FunOrOp (Fun fid) -> ( match fid with | Pure _ -> () diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 3d657ebf..df1f0642 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -489,7 +489,11 @@ let rec translate_sty (span : Meta.span) (ty : T.ty) : ty = | TNever -> craise __FILE__ __LINE__ span "Unreachable" | TRef (_, rty, _) -> translate span rty | TRawPtr (ty, rkind) -> - let mut = match rkind with RMut -> Mut | RShared -> Const in + let mut = + match rkind with + | RMut -> Mut + | RShared -> Const + in let ty = translate span ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) @@ -667,7 +671,11 @@ let rec translate_fwd_ty (span : Meta.span) (type_infos : type_infos) | TLiteral lty -> TLiteral lty | TRef (_, rty, _) -> translate rty | TRawPtr (ty, rkind) -> - let mut = match rkind with RMut -> Mut | RShared -> Const in + let mut = + match rkind with + | RMut -> Mut + | RShared -> Const + in let ty = translate ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) @@ -1805,7 +1813,9 @@ let translate_mplace (p : S.mplace) : mplace = { var_id; name; projection } let translate_opt_mplace (p : S.mplace option) : mplace option = - match p with None -> None | Some p -> Some (translate_mplace p) + match p with + | None -> None + | Some p -> Some (translate_mplace p) (** Explore an abstraction value and convert it to a given back value by collecting all the meta-values from the ended *borrows*. @@ -1864,7 +1874,9 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) in (* Sanity check - Rk.: we do this at every recursive call, which is a bit * expansive... *) - (match value with None -> () | Some value -> type_check_pattern ctx value); + (match value with + | None -> () + | Some value -> type_check_pattern ctx value); (* Return *) (ctx, value) @@ -2075,7 +2087,9 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) If this happens, there are no backward outputs. *) let backward_outputs = - match ctx.backward_outputs with Some outputs -> outputs | None -> [] + match ctx.backward_outputs with + | Some outputs -> outputs + | None -> [] in let field_values = List.map mk_texpression_from_var backward_outputs in mk_simpl_tuple_texpression ctx.span field_values diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index d0b0b7d6..faf888e9 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -36,8 +36,7 @@ let synthesize_symbolic_expansion (span : Meta.span) (sv : symbolic_value) | [ (Some (SeLiteral (VBool true)), true_exp); (Some (SeLiteral (VBool false)), false_exp); - ] -> - ExpandBool (true_exp, false_exp) + ] -> ExpandBool (true_exp, false_exp) | _ -> craise __FILE__ __LINE__ span "Ill-formed boolean expansion") | TLiteral (TInteger int_ty) -> (* Switch over an integer: split between the "regular" branches diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml index 7fb8f7ea..6afff186 100644 --- a/compiler/TypesAnalysis.ml +++ b/compiler/TypesAnalysis.ml @@ -272,7 +272,9 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos) analyze expl_info_init ty_info ty let type_decl_is_opaque (d : type_decl) : bool = - match d.kind with Opaque -> true | _ -> false + match d.kind with + | Opaque -> true + | _ -> false let analyze_type_decl (updated : bool ref) (infos : type_infos) (def : type_decl) : type_infos = diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml index b2c60cc6..f505c470 100644 --- a/compiler/TypesUtils.ml +++ b/compiler/TypesUtils.ml @@ -54,7 +54,9 @@ let raise_if_not_rty_visitor = inherit [_] iter_ty method! visit_region _ r = - match r with RBVar _ | RErased -> raise Found | RStatic | RFVar _ -> () + match r with + | RBVar _ | RErased -> raise Found + | RStatic | RFVar _ -> () end (** Return [true] if the type is a region type (i.e., it doesn't contain erased @@ -71,7 +73,9 @@ let raise_if_not_erased_ty_visitor = inherit [_] iter_ty method! visit_region _ r = - match r with RStatic | RBVar _ | RFVar _ -> raise Found | RErased -> () + match r with + | RStatic | RBVar _ | RFVar _ -> raise Found + | RErased -> () end (** Return [true] if the type is a region type (i.e., it doesn't contain erased regions) *) diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml index 7bb50cad..a1fa40a2 100644 --- a/compiler/ValuesUtils.ml +++ b/compiler/ValuesUtils.ml @@ -43,13 +43,20 @@ let mk_box_value (span : Meta.span) (v : typed_value) : typed_value = let box_v = VAdt { variant_id = None; field_values = [ v ] } in mk_typed_value span box_ty box_v -let is_bottom (v : value) : bool = match v with VBottom -> true | _ -> false +let is_bottom (v : value) : bool = + match v with + | VBottom -> true + | _ -> false let is_aignored (v : avalue) : bool = - match v with AIgnored -> true | _ -> false + match v with + | AIgnored -> true + | _ -> false let is_symbolic (v : value) : bool = - match v with VSymbolic _ -> true | _ -> false + match v with + | VSymbolic _ -> true + | _ -> false let as_symbolic (span : Meta.span) (v : value) : symbolic_value = match v with diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index a7e81535..ffee7b1a 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -9,7 +9,7 @@ Uncaught exception: \nIn file Translate.ml, line 827:\ \nMutually recursive trait declarations are not supported") -Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 47, characters 4-76 +Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 52, characters 4-76 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 853, characters 2-52 Called from Aeneas__Translate.extract_file in file "Translate.ml", line 980, characters 2-36 diff --git a/tests/test_runner/Input.ml b/tests/test_runner/Input.ml index e35be96f..c342a279 100644 --- a/tests/test_runner/Input.ml +++ b/tests/test_runner/Input.ml @@ -43,7 +43,7 @@ let apply_special_comment comment input = let comment = String.trim comment in (* Parse the backends if any *) let re = Re.compile (Re.Pcre.re "^\\[(!)?([a-zA-Z,-]+)\\](.*)$") in - let comment, (backends : Backend.t list) = + let (comment, (backends : Backend.t list)) = match Re.exec_opt re comment with | Some groups -> let exclude = Re.Group.get_opt groups 1 <> None in diff --git a/tests/test_runner/Utils.ml b/tests/test_runner/Utils.ml index 79be617c..2d292929 100644 --- a/tests/test_runner/Utils.ml +++ b/tests/test_runner/Utils.ml @@ -1,11 +1,13 @@ (*** Convenience functions *) let map_while (f : 'a -> 'b option) (input : 'a list) : 'b list = - let _, result = + let (_, result) = List.fold_left (fun (continue, out) a -> if continue then - match f a with None -> (false, out) | Some b -> (true, b :: out) + match f a with + | None -> (false, out) + | Some b -> (true, b :: out) else (continue, out)) (true, []) input in diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 0c3426c5..bac50e84 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -66,7 +66,11 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) = match backend with | Backend.BorrowCheck -> [] | _ -> - let subdir = match subdir with None -> [] | Some x -> [ x ] in + let subdir = + match subdir with + | None -> [] + | Some x -> [ x ] + in [ "-dest"; concat_path ([ env.dest_dir; backend_str ] @ subdir) ] in From 3ee3f7851ce6ffd289a462c58126548839edb146 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 3 Jul 2024 15:31:03 +0200 Subject: [PATCH 04/10] Add curl to the CI environment --- flake.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/flake.nix b/flake.nix index cb3f84ea..37e977d4 100644 --- a/flake.nix +++ b/flake.nix @@ -222,6 +222,7 @@ }; devShells.default = pkgs.mkShell { packages = [ + pkgs.curl pkgs.elan pkgs.ocamlPackages.ocaml pkgs.ocamlPackages.ocamlformat From e7f5c00e91182e4665afe27a3ca03a0d821dcb32 Mon Sep 17 00:00:00 2001 From: Son HO Date: Fri, 5 Jul 2024 14:45:26 +0200 Subject: [PATCH 05/10] Update the Makefile to filter more files when running tests (#280) --- Makefile | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Makefile b/Makefile index 1e832378..2b4bd990 100644 --- a/Makefile +++ b/Makefile @@ -154,6 +154,8 @@ verify: INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*) # Remove the committed output files INPUTS_LIST := $(filter-out %.out,$(INPUTS_LIST)) +# Remove some temporary files which are inserted by, for instance, Emacs +INPUTS_LIST := $(filter-out %~,$(INPUTS_LIST)) # Remove the directory prefix, replace with `test-` INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST)) From 71f2c2a4f7c50ce11d0d90d31135972c386b2831 Mon Sep 17 00:00:00 2001 From: Ryan Lahfa Date: Fri, 5 Jul 2024 15:25:11 +0200 Subject: [PATCH 06/10] feat: progress? to say which theorem has been used (#277) Like `simp?` and similar, `progress?` will provide what theorem was used to make the goal progress. Signed-off-by: Ryan Lahfa Co-authored-by: Ryan Lahfa Co-authored-by: Son HO --- backends/lean/Base/Progress/Progress.lean | 61 +++++++++++++++++++---- 1 file changed, 51 insertions(+), 10 deletions(-) diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 35cc8399..cea46da8 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -33,9 +33,15 @@ inductive TheoremOrLocal where | Theorem (thName : Name) | Local (asm : LocalDecl) +structure Stats where + usedTheorem : TheoremOrLocal + instance : ToMessageData TheoremOrLocal where toMessageData := λ x => match x with | .Theorem thName => m!"{thName}" | .Local asm => m!"{asm.userName}" +instance : Coe TheoremOrLocal Name where + coe := λ x => match x with | .Theorem thName => thName | .Local asm => asm.userName + /- Type to propagate the errors of `progressWith`. We need this because we use the exceptions to backtrack, when trying to use the assumptions for instance. When there is actually an error we want @@ -234,7 +240,7 @@ def tryLookupApply (keep : Option Name) (ids : Array (Option Name)) (splitPost : -- The array of ids are identifiers to use when introducing fresh variables def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrLocal) - (ids : Array (Option Name)) (splitPost : Bool) (asmTac : TacticM Unit) : TacticM Unit := do + (ids : Array (Option Name)) (splitPost : Bool) (asmTac : TacticM Unit) : TacticM TheoremOrLocal := do withMainContext do -- Retrieve the goal let mgoal ← Tactic.getMainGoal @@ -262,7 +268,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL match withTh with | some th => do match ← progressWith fExpr th keep ids splitPost asmTac with - | .Ok => return () + | .Ok => return th | .Error msg => throwError msg | none => -- Try all the assumptions one by one and if it fails try to lookup a theorem. @@ -272,7 +278,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL trace[Progress] "Trying assumption: {decl.userName} : {decl.type}" let res ← do try progressWith fExpr (.Local decl) keep ids splitPost asmTac catch _ => continue match res with - | .Ok => return () + | .Ok => return (.Local decl) | .Error msg => throwError msg -- It failed: lookup the pspec theorems which match the expression *only -- if the function is a constant* @@ -293,7 +299,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL pure (thNames.map fun th => TheoremOrLocal.Theorem th) -- Try the theorems one by one for pspec in pspecs do - if ← tryLookupApply keep ids splitPost asmTac fExpr "pspec theorem" pspec then return () + if ← tryLookupApply keep ids splitPost asmTac fExpr "pspec theorem" pspec then return pspec else pure () -- It failed: try to use the recursive assumptions trace[Progress] "Failed using a pspec theorem: trying to use a recursive assumption" @@ -306,14 +312,14 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL trace[Progress] "Trying recursive assumption: {decl.userName} : {decl.type}" let res ← do try progressWith fExpr (.Local decl) keep ids splitPost asmTac catch _ => continue match res with - | .Ok => return () + | .Ok => return (.Local decl) | .Error msg => throwError msg -- Nothing worked: failed throwError "Progress failed" syntax progressArgs := ("keep" (ident <|> "_"))? ("with" ident)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")? -def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do +def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Stats := do let args := args.raw -- Process the arguments to retrieve the identifiers to use trace[Progress] "Progress arguments: {args}" @@ -370,14 +376,26 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do Arith.scalarTac false else throwError "Not a linear arithmetic goal" - progressAsmsOrLookupTheorem keep withArg ids splitPost ( + let usedTheorem ← progressAsmsOrLookupTheorem keep withArg ids splitPost ( withMainContext do trace[Progress] "trying to solve assumption: {← getMainGoal}" firstTac [assumptionTac, scalarTac]) - trace[Diverge] "Progress done" + trace[Progress] "Progress done" + return { + usedTheorem + } + +elab (name := progress) "progress" args:progressArgs : tactic => + evalProgress args *> return () -elab "progress" args:progressArgs : tactic => - evalProgress args +elab tk:"progress?" args:progressArgs : tactic => do + let stats ← evalProgress args + let mut stxArgs := args.raw + if stxArgs[1].isNone then + let withArg := mkNullNode #[mkAtom "with", mkIdent stats.usedTheorem] + stxArgs := stxArgs.setArg 1 withArg + let tac := mkNode `Progress.progress #[mkAtom "progress", stxArgs] + Meta.Tactic.TryThis.addSuggestion tk tac (origSpan? := ← getRef) namespace Test open Primitives Result @@ -386,6 +404,8 @@ namespace Test -- set_option trace.Progress true -- set_option pp.rawOnError true + set_option says.verify true + -- The following commands display the databases of theorems -- #eval showStoredPSpec open alloc.vec @@ -397,6 +417,13 @@ namespace Test progress keep _ as ⟨ z, h1 .. ⟩ simp [*, h1] + example {ty} {x y : Scalar ty} + (hmin : Scalar.min ty ≤ x.val + y.val) + (hmax : x.val + y.val ≤ Scalar.max ty) : + ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by + progress? keep _ as ⟨ z, h1 .. ⟩ says progress keep _ with Primitives.Scalar.add_spec as ⟨ z, h1 .. ⟩ + simp [*, h1] + example {ty} {x y : Scalar ty} (hmin : Scalar.min ty ≤ x.val + y.val) (hmax : x.val + y.val ≤ Scalar.max ty) : @@ -432,6 +459,14 @@ namespace Test progress simp [*] + + example {α : Type} (v: Vec α) (i: Usize) (x : α) + (hbounds : i.val < v.length) : + ∃ nv, v.update_usize i x = ok nv ∧ + nv.val = v.val.update i.val x := by + progress? says progress with Primitives.alloc.vec.Vec.update_usize_spec + simp [*] + /- Checking that progress can handle nested blocks -/ example {α : Type} (v: Vec α) (i: Usize) (x : α) (hbounds : i.val < v.length) : @@ -454,6 +489,12 @@ namespace Test f x = ok () := by progress + + example {x : U32} + (f : U32 → Result Unit) (h : ∀ x, f x = .ok ()) : + f x = ok () := by + progress? says progress with h + /- The use of `right` introduces a meta-variable in the goal, that we need to instantiate (otherwise `progress` gets stuck) -/ example {ty} {x y : Scalar ty} From 7d5801fcf230593ee500af45c63eda50f3b69163 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 8 Jul 2024 11:29:28 +0200 Subject: [PATCH 07/10] Remove redundant output of `norm_ctx_normalize_trait_instance_id` --- compiler/AssociatedTypes.ml | 86 ++++++++++++++++++------------------- 1 file changed, 43 insertions(+), 43 deletions(-) diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 90a1714f..9bc3673f 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -350,27 +350,21 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = over it. *) and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) - (id : trait_instance_id) : trait_instance_id * trait_ref option = + (id : trait_instance_id) : trait_instance_id = match id with - | Self -> (id, None) + | Self -> id | TraitImpl _ -> (* The [TraitImpl] shouldn't be inside any projection - we check this elsewhere by asserting that whenever we return [None] for the impl trait ref, then the id actually refers to a local clause. *) - (id, None) - | Clause _ -> (id, None) - | BuiltinOrAuto _ -> (id, None) - | ParentClause (inst_id, decl_id, clause_id) -> ( - let inst_id, impl = norm_ctx_normalize_trait_instance_id ctx inst_id in + id + | Clause _ -> id + | BuiltinOrAuto _ -> id + | ParentClause (inst_id, decl_id, clause_id) -> begin + let inst_id = norm_ctx_normalize_trait_instance_id ctx inst_id in (* Check if the inst_id refers to a specific implementation, if yes project *) - match impl with - | None -> - (* This is actually a local clause *) - sanity_check_opt_span __FILE__ __LINE__ - (trait_instance_id_is_local_clause inst_id) - ctx.span; - (ParentClause (inst_id, decl_id, clause_id), None) - | Some impl -> + match inst_id with + | TraitRef impl -> (* We figure out the parent clause by doing the following: {[ // The implementation we are looking at @@ -392,18 +386,19 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) in (* Normalize the clause *) let clause = norm_ctx_normalize_trait_ref ctx clause in - (TraitRef clause, Some clause)) - | ItemClause (inst_id, decl_id, item_name, clause_id) -> ( - let inst_id, impl = norm_ctx_normalize_trait_instance_id ctx inst_id in - (* Check if the inst_id refers to a specific implementation, if yes project *) - match impl with - | None -> + TraitRef clause + | _ -> (* This is actually a local clause *) sanity_check_opt_span __FILE__ __LINE__ (trait_instance_id_is_local_clause inst_id) ctx.span; - (ItemClause (inst_id, decl_id, item_name, clause_id), None) - | Some impl -> + ParentClause (inst_id, decl_id, clause_id) + end + | ItemClause (inst_id, decl_id, item_name, clause_id) -> begin + let inst_id = norm_ctx_normalize_trait_instance_id ctx inst_id in + (* Check if the inst_id refers to a specific implementation, if yes project *) + match inst_id with + | TraitRef impl -> (* We figure out the item clause by doing the following: {[ // The implementation we are looking at @@ -425,7 +420,14 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) in (* Normalize the clause *) let clause = norm_ctx_normalize_trait_ref ctx clause in - (TraitRef clause, Some clause)) + TraitRef clause + | _ -> + (* This is actually a local clause *) + sanity_check_opt_span __FILE__ __LINE__ + (trait_instance_id_is_local_clause inst_id) + ctx.span; + ItemClause (inst_id, decl_id, item_name, clause_id) + end | TraitRef { trait_id = TraitImpl trait_id; generics; trait_decl_ref } -> (* We can't simplify the id *yet* : we will simplify it when projecting. However, we have an implementation to return *) @@ -437,7 +439,7 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) let trait_ref : trait_ref = { trait_id = TraitImpl trait_id; generics; trait_decl_ref } in - (TraitRef trait_ref, Some trait_ref) + TraitRef trait_ref | TraitRef trait_ref -> (* The trait instance id necessarily refers to a local sub-clause. We can't project over it and can only peel off the [TraitRef] wrapper *) @@ -447,18 +449,18 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) sanity_check_opt_span __FILE__ __LINE__ (trait_ref.generics = empty_generic_args) ctx.span; - (trait_ref.trait_id, None) + trait_ref.trait_id | FnPointer ty -> let ty = norm_ctx_normalize_ty ctx ty in (* TODO: we might want to return the ref to the function pointer, in order to later normalize a call to this function pointer *) - (FnPointer ty, None) + FnPointer ty | Closure (fid, generics) -> let generics = norm_ctx_normalize_generic_args ctx generics in - (Closure (fid, generics), None) + Closure (fid, generics) | Unsolved _ | UnknownTrait _ -> (* This is actually an error case *) - (id, None) + id | Dyn _ -> craise_opt_span __FILE__ __LINE__ ctx.span "Dynamic trait types are not supported yet" @@ -479,11 +481,18 @@ and norm_ctx_normalize_trait_ref (ctx : norm_ctx) (trait_ref : trait_ref) : ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref)); let { trait_id; generics; trait_decl_ref } = trait_ref in (* Check if the id is an impl, otherwise normalize it *) - let trait_id, norm_trait_ref = - norm_ctx_normalize_trait_instance_id ctx trait_id - in - match norm_trait_ref with - | None -> + let trait_id = norm_ctx_normalize_trait_instance_id ctx trait_id in + match trait_id with + | TraitRef trait_ref -> + log#ldebug + (lazy + ("norm_ctx_normalize_trait_ref: normalized to: " + ^ trait_ref_to_string ctx trait_ref)); + sanity_check_opt_span __FILE__ __LINE__ + (generics = empty_generic_args) + ctx.span; + trait_ref + | _ -> log#ldebug (lazy ("norm_ctx_normalize_trait_ref: no norm: " @@ -493,15 +502,6 @@ and norm_ctx_normalize_trait_ref (ctx : norm_ctx) (trait_ref : trait_ref) : norm_ctx_normalize_trait_decl_ref ctx trait_decl_ref in { trait_id; generics; trait_decl_ref } - | Some trait_ref -> - log#ldebug - (lazy - ("norm_ctx_normalize_trait_ref: normalized to: " - ^ trait_ref_to_string ctx trait_ref)); - sanity_check_opt_span __FILE__ __LINE__ - (generics = empty_generic_args) - ctx.span; - trait_ref (* Not sure this one is really necessary *) and norm_ctx_normalize_trait_decl_ref (ctx : norm_ctx) From 1266479da0d07a51c05b998c14b8f13a523130a8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 8 Jul 2024 10:10:40 +0200 Subject: [PATCH 08/10] Update charon --- charon-pin | 2 +- compiler/AssociatedTypes.ml | 106 +++++++----------------------- compiler/ExtractBase.ml | 4 +- compiler/ExtractTypes.ml | 50 ++++++-------- compiler/Interpreter.ml | 8 +-- compiler/InterpreterStatements.ml | 12 ++-- compiler/PrintPure.ml | 25 ++++--- compiler/Pure.ml | 4 +- compiler/PureUtils.ml | 2 +- compiler/SymbolicToPure.ml | 20 +++--- flake.lock | 12 ++-- 11 files changed, 88 insertions(+), 157 deletions(-) diff --git a/charon-pin b/charon-pin index afc5bfae..d27a488d 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -e0bf68d674edbb154fe2343b2315ccac325a0c7a +cccc38353eec92c32c0f7a755fcef4ab5b1ae863 diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 9bc3673f..dc1aa67d 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -94,16 +94,15 @@ let ctx_add_norm_trait_types_from_preds (span : Meta.span) (ctx : eval_ctx) let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool = match id with | Self | Clause _ -> true + | ParentClause (id, _, _) | ItemClause (id, _, _, _) -> + trait_instance_id_is_local_clause id | TraitImpl _ | BuiltinOrAuto _ - | TraitRef _ | UnknownTrait _ | FnPointer _ | Closure _ | Unsolved _ | Dyn _ -> false - | ParentClause (id, _, _) | ItemClause (id, _, _, _) -> - trait_instance_id_is_local_clause id (** About the conversion functions: for now we need them (TODO: merge ety, rty, etc.), but they should be applied to types without regions. @@ -149,6 +148,10 @@ let trait_ref_to_string (ctx : norm_ctx) (x : trait_ref) : string = let ctx = norm_ctx_to_fmt_env ctx in Print.Types.trait_ref_to_string ctx x +let trait_decl_ref_to_string (ctx : norm_ctx) (x : trait_decl_ref) : string = + let ctx = norm_ctx_to_fmt_env ctx in + Print.Types.trait_decl_ref_to_string ctx x + let trait_instance_id_to_string (ctx : norm_ctx) (x : trait_instance_id) : string = let ctx = norm_ctx_to_fmt_env ctx in @@ -247,23 +250,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in let ty : ty = match trait_ref.trait_id with - | TraitRef { trait_id = TraitImpl impl_id; generics = ref_generics; _ } - -> - cassert_opt_span __FILE__ __LINE__ - (ref_generics = empty_generic_args) - ctx.span "Higher order trait types are not supported yet"; - log#ldebug - (lazy - ("norm_ctx_normalize_ty: trait type: trait ref: " - ^ ty_to_string ctx ty)); - (* Lookup the type *) - let ty = - norm_ctx_lookup_trait_impl_ty ctx impl_id trait_ref.generics - type_name - in - (* Normalize *) - norm_ctx_normalize_ty ctx ty - | TraitImpl impl_id -> + | TraitImpl (impl_id, generics) -> log#ldebug (lazy ("norm_ctx_normalize_ty (trait impl):\n- trait type: " @@ -278,8 +265,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = *) (* Lookup the type *) let ty = - norm_ctx_lookup_trait_impl_ty ctx impl_id trait_ref.generics - type_name + norm_ctx_lookup_trait_impl_ty ctx impl_id generics type_name in (* Normalize *) norm_ctx_normalize_ty ctx ty @@ -353,18 +339,19 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) (id : trait_instance_id) : trait_instance_id = match id with | Self -> id - | TraitImpl _ -> + | TraitImpl (impl_id, generics) -> (* The [TraitImpl] shouldn't be inside any projection - we check this elsewhere by asserting that whenever we return [None] for the impl trait ref, then the id actually refers to a local clause. *) - id + let generics = norm_ctx_normalize_generic_args ctx generics in + TraitImpl (impl_id, generics) | Clause _ -> id | BuiltinOrAuto _ -> id | ParentClause (inst_id, decl_id, clause_id) -> begin let inst_id = norm_ctx_normalize_trait_instance_id ctx inst_id in (* Check if the inst_id refers to a specific implementation, if yes project *) match inst_id with - | TraitRef impl -> + | TraitImpl (impl_id, generics) -> (* We figure out the parent clause by doing the following: {[ // The implementation we are looking at @@ -377,16 +364,12 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) ]} *) (* Lookup the clause *) - let impl_id = - TypesUtils.trait_instance_id_as_trait_impl impl.trait_id - in let clause = - norm_ctx_lookup_trait_impl_parent_clause ctx impl_id impl.generics + norm_ctx_lookup_trait_impl_parent_clause ctx impl_id generics clause_id in (* Normalize the clause *) - let clause = norm_ctx_normalize_trait_ref ctx clause in - TraitRef clause + norm_ctx_normalize_trait_instance_id ctx clause.trait_id | _ -> (* This is actually a local clause *) sanity_check_opt_span __FILE__ __LINE__ @@ -398,7 +381,7 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) let inst_id = norm_ctx_normalize_trait_instance_id ctx inst_id in (* Check if the inst_id refers to a specific implementation, if yes project *) match inst_id with - | TraitRef impl -> + | TraitImpl (impl_id, generics) -> (* We figure out the item clause by doing the following: {[ // The implementation we are looking at @@ -411,16 +394,12 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) ]} *) (* Lookup the impl *) - let impl_id = - TypesUtils.trait_instance_id_as_trait_impl impl.trait_id - in let clause = - norm_ctx_lookup_trait_impl_item_clause ctx impl_id impl.generics + norm_ctx_lookup_trait_impl_item_clause ctx impl_id generics item_name clause_id in (* Normalize the clause *) - let clause = norm_ctx_normalize_trait_ref ctx clause in - TraitRef clause + norm_ctx_normalize_trait_instance_id ctx clause.trait_id | _ -> (* This is actually a local clause *) sanity_check_opt_span __FILE__ __LINE__ @@ -428,28 +407,6 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) ctx.span; ItemClause (inst_id, decl_id, item_name, clause_id) end - | TraitRef { trait_id = TraitImpl trait_id; generics; trait_decl_ref } -> - (* We can't simplify the id *yet* : we will simplify it when projecting. - However, we have an implementation to return *) - (* Normalize the generics *) - let generics = norm_ctx_normalize_generic_args ctx generics in - let trait_decl_ref = - norm_ctx_normalize_trait_decl_ref ctx trait_decl_ref - in - let trait_ref : trait_ref = - { trait_id = TraitImpl trait_id; generics; trait_decl_ref } - in - TraitRef trait_ref - | TraitRef trait_ref -> - (* The trait instance id necessarily refers to a local sub-clause. We - can't project over it and can only peel off the [TraitRef] wrapper *) - sanity_check_opt_span __FILE__ __LINE__ - (trait_instance_id_is_local_clause trait_ref.trait_id) - ctx.span; - sanity_check_opt_span __FILE__ __LINE__ - (trait_ref.generics = empty_generic_args) - ctx.span; - trait_ref.trait_id | FnPointer ty -> let ty = norm_ctx_normalize_ty ctx ty in (* TODO: we might want to return the ref to the function pointer, @@ -479,29 +436,16 @@ and norm_ctx_normalize_trait_ref (ctx : norm_ctx) (trait_ref : trait_ref) : ("norm_ctx_normalize_trait_ref: " ^ trait_ref_to_string ctx trait_ref ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref)); - let { trait_id; generics; trait_decl_ref } = trait_ref in + let { trait_id; trait_decl_ref } = trait_ref in + (* Check if the id is an impl, otherwise normalize it *) let trait_id = norm_ctx_normalize_trait_instance_id ctx trait_id in - match trait_id with - | TraitRef trait_ref -> - log#ldebug - (lazy - ("norm_ctx_normalize_trait_ref: normalized to: " - ^ trait_ref_to_string ctx trait_ref)); - sanity_check_opt_span __FILE__ __LINE__ - (generics = empty_generic_args) - ctx.span; - trait_ref - | _ -> - log#ldebug - (lazy - ("norm_ctx_normalize_trait_ref: no norm: " - ^ trait_instance_id_to_string ctx trait_id)); - let generics = norm_ctx_normalize_generic_args ctx generics in - let trait_decl_ref = - norm_ctx_normalize_trait_decl_ref ctx trait_decl_ref - in - { trait_id; generics; trait_decl_ref } + let trait_decl_ref = norm_ctx_normalize_trait_decl_ref ctx trait_decl_ref in + log#ldebug + (lazy + ("norm_ctx_normalize_trait_ref: no norm: " + ^ trait_instance_id_to_string ctx trait_id)); + { trait_id; trait_decl_ref } (* Not sure this one is really necessary *) and norm_ctx_normalize_trait_decl_ref (ctx : norm_ctx) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 52a163eb..c3f6fa59 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1641,9 +1641,9 @@ let ctx_compute_trait_clause_name (ctx : extraction_ctx) (fun (c : Types.trait_clause) -> c.clause_id = clause_id) clauses in - let trait_id = clause.trait_id in + let trait_id = clause.trait.trait_decl_id in let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in - let args = clause.clause_generics in + let args = clause.trait.decl_generics in trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix impl_trait_decl.item_meta.name params args in diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 6b196548..aac39924 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -587,9 +587,6 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) *) match trait_ref.trait_id with | Self -> - sanity_check __FILE__ __LINE__ - (trait_ref.generics = empty_generic_args) - span; extract_trait_instance_id_with_dot span ctx fmt no_params_tys false trait_ref.trait_id; F.pp_print_string fmt type_name @@ -606,28 +603,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) and extract_trait_ref (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool) (tr : trait_ref) : unit = - let use_brackets = tr.generics <> empty_generic_args && inside in - if use_brackets then F.pp_print_string fmt "("; - (* We may need to filter the parameters if the trait is builtin *) - let generics = - match tr.trait_id with - | TraitImpl id -> ( - match - TraitImplId.Map.find_opt id ctx.trait_impls_filter_type_args_map - with - | None -> tr.generics - | Some filter -> - let types = - List.filter_map - (fun (b, x) -> if b then Some x else None) - (List.combine filter tr.generics.types) - in - { tr.generics with types }) - | _ -> tr.generics - in - extract_trait_instance_id span ctx fmt no_params_tys inside tr.trait_id; - extract_generic_args span ctx fmt no_params_tys generics; - if use_brackets then F.pp_print_string fmt ")" + extract_trait_instance_id span ctx fmt no_params_tys inside tr.trait_id and extract_trait_decl_ref (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool) @@ -715,9 +691,27 @@ and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx) (associated type, etc.). We should have caught this elsewhere. *) save_error __FILE__ __LINE__ (Some span) "Unexpected occurrence of `Self`"; F.pp_print_string fmt "ERROR(\"Unexpected Self\")" - | TraitImpl id -> + | TraitImpl (id, generics) -> + (* We may need to filter the parameters if the trait is builtin *) + let generics = + match + TraitImplId.Map.find_opt id ctx.trait_impls_filter_type_args_map + with + | None -> generics + | Some filter -> + let types = + List.filter_map + (fun (b, x) -> if b then Some x else None) + (List.combine filter generics.types) + in + { generics with types } + in let name = ctx_get_trait_impl span id ctx in - F.pp_print_string fmt name + let use_brackets = generics <> empty_generic_args && inside in + if use_brackets then F.pp_print_string fmt "("; + F.pp_print_string fmt name; + extract_generic_args span ctx fmt no_params_tys generics; + if use_brackets then F.pp_print_string fmt ")" | Clause id -> let name = ctx_get_local_trait_clause span id ctx in F.pp_print_string fmt name @@ -733,8 +727,6 @@ and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx) in extract_trait_instance_id_with_dot span ctx fmt no_params_tys true inst_id; F.pp_print_string fmt (add_brackets name) - | TraitRef trait_ref -> - extract_trait_ref span ctx fmt no_params_tys inside trait_ref | UnknownTrait _ -> (* This is an error case *) craise __FILE__ __LINE__ span "Unexpected" diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 3d665de6..91613eeb 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -133,17 +133,15 @@ let symbolic_instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx) List.fold_left_map (fun tr_map (c : trait_clause) -> let subst = mk_subst tr_map in - let { trait_id = trait_decl_id; clause_generics; _ } = c in + let { trait_decl_id; decl_generics; _ } = c.trait in let generics = - Substitute.generic_args_substitute subst clause_generics + Substitute.generic_args_substitute subst decl_generics in let trait_decl_ref = { trait_decl_id; decl_generics = generics } in (* Note that because we directly refer to the clause, we give it empty generics *) let trait_id = Clause c.clause_id in - let trait_ref = - { trait_id; generics = empty_generic_args; trait_decl_ref } - in + let trait_ref = { trait_id; trait_decl_ref } in (* Update the traits map *) let tr_map = TraitClauseId.Map.add c.clause_id trait_id tr_map in (tr_map, trait_ref)) diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index cf104d77..c4f26008 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -753,7 +753,7 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span) depending on whethere we call a top-level trait method impl or the method from a local clause *) match trait_ref.trait_id with - | TraitImpl impl_id -> ( + | TraitImpl (impl_id, generics) -> ( (* Lookup the trait impl *) let trait_impl = ctx_lookup_trait_impl ctx impl_id in log#ldebug @@ -770,11 +770,9 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span) let method_def = ctx_lookup_fun_decl ctx id in (* We have to concatenate the generics for the impl and the generics for the method *) - let generics = - merge_generic_args trait_ref.generics func.generics - in + let generics = merge_generic_args generics func.generics in (* Instantiate *) - let tr_self = TraitRef trait_ref in + let tr_self = trait_ref.trait_id in let fid : fun_id = FRegular id in let regions_hierarchy = LlbcAstUtils.FunIdMap.find fid @@ -847,7 +845,7 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span) LlbcAstUtils.FunIdMap.find (FRegular method_id) ctx.fun_ctx.regions_hierarchies in - let tr_self = TraitRef trait_ref in + let tr_self = trait_ref.trait_id in let inst_sg = instantiate_fun_sig span ctx all_generics tr_self method_def.signature regions_hierarchy @@ -891,7 +889,7 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span) LlbcAstUtils.FunIdMap.find (FRegular method_id) ctx.fun_ctx.regions_hierarchies in - let tr_self = TraitRef trait_ref in + let tr_self = trait_ref.trait_id in let inst_sg = instantiate_fun_sig span ctx generics tr_self method_def.signature regions_hierarchy diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index a142aa8f..3d679622 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -177,26 +177,31 @@ and generic_args_to_string (env : fmt_env) (generics : generic_args) : string = and trait_ref_to_string (env : fmt_env) (inside : bool) (tr : trait_ref) : string = - let trait_id = trait_instance_id_to_string env false tr.trait_id in - let generics = generic_args_to_string env tr.generics in - let s = trait_id ^ generics in - if tr.generics = empty_generic_args || not inside then s else "(" ^ s ^ ")" + let trait_id = trait_instance_id_to_string env tr.trait_id in + let generics_are_empty = + match tr.trait_id with + | TraitImpl (_, generics) -> generics = empty_generic_args + | _ -> true + in + if generics_are_empty || not inside then trait_id else "(" ^ trait_id ^ ")" -and trait_instance_id_to_string (env : fmt_env) (inside : bool) - (id : trait_instance_id) : string = +and trait_instance_id_to_string (env : fmt_env) (id : trait_instance_id) : + string = match id with | Self -> "Self" - | TraitImpl id -> trait_impl_id_to_string env id + | TraitImpl (impl_id, generics) -> + let generics = generic_args_to_string env generics in + let impl_id = trait_impl_id_to_string env impl_id in + impl_id ^ generics | Clause id -> trait_clause_id_to_string env id | ParentClause (inst_id, _decl_id, clause_id) -> - let inst_id = trait_instance_id_to_string env false inst_id in + let inst_id = trait_instance_id_to_string env inst_id in let clause_id = trait_clause_id_to_string env clause_id in "parent(" ^ inst_id ^ ")::" ^ clause_id | ItemClause (inst_id, _decl_id, item_name, clause_id) -> - let inst_id = trait_instance_id_to_string env false inst_id in + let inst_id = trait_instance_id_to_string env inst_id in let clause_id = trait_clause_id_to_string env clause_id in "(" ^ inst_id ^ ")::" ^ item_name ^ "::[" ^ clause_id ^ "]" - | TraitRef tr -> trait_ref_to_string env inside tr | UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")" let trait_clause_to_string (env : fmt_env) (clause : trait_clause) : string = diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 2754eaac..0575dce1 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -290,7 +290,6 @@ type ty = and trait_ref = { trait_id : trait_instance_id; - generics : generic_args; trait_decl_ref : trait_decl_ref; } @@ -307,12 +306,11 @@ and generic_args = { and trait_instance_id = | Self - | TraitImpl of trait_impl_id + | TraitImpl of trait_impl_id * generic_args | Clause of trait_clause_id | ParentClause of trait_instance_id * trait_decl_id * trait_clause_id | ItemClause of trait_instance_id * trait_decl_id * trait_item_name * trait_clause_id - | TraitRef of trait_ref | UnknownTrait of string [@@deriving show, diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 579b3dd5..818e4f8b 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -163,7 +163,7 @@ let make_const_generic_subst (vars : const_generic_var list) let make_trait_subst (clauses : trait_clause list) (refs : trait_ref list) : TraitClauseId.id -> trait_instance_id = let clauses = List.map (fun x -> x.clause_id) clauses in - let refs = List.map (fun x -> TraitRef x) refs in + let refs = List.map (fun (x : trait_ref) -> x.trait_id) refs in let ls = List.combine clauses refs in let mp = List.fold_left diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index df1f0642..29af3efc 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -422,11 +422,10 @@ let rec translate_generic_args (span : Meta.span) (translate_ty : T.ty -> ty) and translate_trait_ref (span : Meta.span) (translate_ty : T.ty -> ty) (tr : T.trait_ref) : trait_ref = let trait_id = translate_trait_instance_id span translate_ty tr.trait_id in - let generics = translate_generic_args span translate_ty tr.generics in let trait_decl_ref = translate_trait_decl_ref span translate_ty tr.trait_decl_ref in - { trait_id; generics; trait_decl_ref } + { trait_id; trait_decl_ref } and translate_trait_decl_ref (span : Meta.span) (translate_ty : T.ty -> ty) (tr : T.trait_decl_ref) : trait_decl_ref = @@ -442,7 +441,9 @@ and translate_trait_instance_id (span : Meta.span) (translate_ty : T.ty -> ty) in match id with | T.Self -> Self - | TraitImpl id -> TraitImpl id + | TraitImpl (id, generics) -> + let generics = translate_generic_args span translate_ty generics in + TraitImpl (id, generics) | BuiltinOrAuto _ -> (* We should have eliminated those in the prepasses *) craise __FILE__ __LINE__ span "Unreachable" @@ -453,7 +454,6 @@ and translate_trait_instance_id (span : Meta.span) (translate_ty : T.ty -> ty) | ItemClause (inst_id, decl_id, item_name, clause_id) -> let inst_id = translate_trait_instance_id inst_id in ItemClause (inst_id, decl_id, item_name, clause_id) - | TraitRef tr -> TraitRef (translate_trait_ref span translate_ty tr) | FnPointer _ | Closure _ -> craise __FILE__ __LINE__ span "Closures are not supported yet" | Dyn _ -> @@ -518,9 +518,9 @@ and translate_strait_instance_id (span : Meta.span) (id : T.trait_instance_id) : let translate_trait_clause (span : Meta.span) (clause : T.trait_clause) : trait_clause = - let { T.clause_id; span = _; trait_id; clause_generics } = clause in - let generics = translate_sgeneric_args span clause_generics in - { clause_id; trait_id; generics } + let { T.clause_id; span = _; trait } = clause in + let generics = translate_sgeneric_args span trait.decl_generics in + { clause_id; trait_id = trait.trait_decl_id; generics } let translate_strait_type_constraint (span : Meta.span) (ttc : T.trait_type_constraint) : trait_type_constraint = @@ -3576,11 +3576,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = let trait_decl_ref = { trait_decl_id = c.trait_id; decl_generics = empty_generic_args } in - { - trait_id = Clause c.clause_id; - generics = empty_generic_args; - trait_decl_ref; - }) + { trait_id = Clause c.clause_id; trait_decl_ref }) trait_clauses in { types; const_generics; trait_refs } diff --git a/flake.lock b/flake.lock index 8ee72978..4f5b189a 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1719994894, - "narHash": "sha256-RhSc57vv/xORPkjqnL4jcupcyV6DTfgm8KqRiOI1ruA=", + "lastModified": 1720447930, + "narHash": "sha256-U5Tz1Pz7pmeFTrheZS90K3iRmfnlHvi47UexXflwV2o=", "owner": "aeneasverif", "repo": "charon", - "rev": "e0bf68d674edbb154fe2343b2315ccac325a0c7a", + "rev": "cccc38353eec92c32c0f7a755fcef4ab5b1ae863", "type": "github" }, "original": { @@ -272,11 +272,11 @@ ] }, "locked": { - "lastModified": 1719973106, - "narHash": "sha256-IGCdN/m7DfwUfxZjFnlTiTtpwSHCb01P/LWavAKD2jw=", + "lastModified": 1720405186, + "narHash": "sha256-7D57KwmTIbsopE/1g8hFeIbVoeJGgU3wfuGYvTlNQG4=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "fb733500aead50880b9b301f34a0061bf997d6f2", + "rev": "f0ca58b37ff4179ce4587589c32205764d9b4a4f", "type": "github" }, "original": { From 769e55c85442a97d0045a0e6c9f249b8a6b7638c Mon Sep 17 00:00:00 2001 From: Ryan Lahfa Date: Tue, 9 Jul 2024 15:59:09 +0200 Subject: [PATCH 09/10] chore: add rustup for completeness Otherwise, `make test` won't build out of the box. Signed-off-by: Ryan Lahfa --- flake.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/flake.nix b/flake.nix index 37e977d4..9b7717fb 100644 --- a/flake.nix +++ b/flake.nix @@ -229,6 +229,7 @@ pkgs.ocamlPackages.menhir pkgs.ocamlPackages.odoc pkgs.jq + pkgs.rustup ]; inputsFrom = [ From d5e163d96cbc5e7d84da15102cd91e3df0c34949 Mon Sep 17 00:00:00 2001 From: Ryan Lahfa Date: Tue, 9 Jul 2024 15:57:05 +0200 Subject: [PATCH 10/10] doc: initialize a user-facing mdbook Design: - A flake similar to leanprover/lean4?subdir=docs/... - Alectryon + Lean-mdBook - CI + build Signed-off-by: Ryan Lahfa --- .github/workflows/build-userdocs.yml | 12 ++ .github/workflows/deploy-userdocs.yml | 32 ++++ docs/user/.envrc | 1 + docs/user/.gitignore | 1 + docs/user/book.toml | 6 + docs/user/flake.lock | 256 +++++++++++++++++++++++++ docs/user/flake.nix | 110 +++++++++++ docs/user/src/README.md | 16 ++ docs/user/src/SUMMARY.md | 11 ++ docs/user/src/lean/tactics/progress.md | 2 + 10 files changed, 447 insertions(+) create mode 100644 .github/workflows/build-userdocs.yml create mode 100644 .github/workflows/deploy-userdocs.yml create mode 100644 docs/user/.envrc create mode 100644 docs/user/.gitignore create mode 100644 docs/user/book.toml create mode 100644 docs/user/flake.lock create mode 100644 docs/user/flake.nix create mode 100644 docs/user/src/README.md create mode 100644 docs/user/src/SUMMARY.md create mode 100644 docs/user/src/lean/tactics/progress.md diff --git a/.github/workflows/build-userdocs.yml b/.github/workflows/build-userdocs.yml new file mode 100644 index 00000000..57078e99 --- /dev/null +++ b/.github/workflows/build-userdocs.yml @@ -0,0 +1,12 @@ +name: Build Aeneas user docs and test them +on: [push, pull_request] + +jobs: + test: + name: Test Aeneas user docs + runs-on: [self-hosted, linux, nix] + steps: + - uses: actions/checkout@v4 + - name: Build the book + run: nix build '.?dir=docs/user'#book + # TODO: test the Lean examples code via nix build '.?dir=docs/user'#test or something similar. diff --git a/.github/workflows/deploy-userdocs.yml b/.github/workflows/deploy-userdocs.yml new file mode 100644 index 00000000..88f6b57c --- /dev/null +++ b/.github/workflows/deploy-userdocs.yml @@ -0,0 +1,32 @@ +name: Deploy Aeneas user docs to GitHub pages +on: + push: + branches: + - main + +jobs: + deploy: + runs-on: [self-hosted, linux, nix] + permissions: + contents: write # To push a branch + pull-requests: write # To create a PR from that branch + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + - name: Deploy GitHub Pages + run: | + # This assumes your book is in the root of your repository. + # Just add a `cd` here if you need to change to another directory. + nix build '.?dir=docs/user'#book -o html + git worktree add gh-pages + git config user.name "Deploy from CI" + git config user.email "" + cd gh-pages + # Delete the ref to avoid keeping history. + git update-ref -d refs/heads/gh-pages + rm -rf * + cp --dereference -vr ../html/* . + git add . + git commit -m "Deploy $GITHUB_SHA to gh-pages" + git push --force --set-upstream origin gh-pages diff --git a/docs/user/.envrc b/docs/user/.envrc new file mode 100644 index 00000000..3550a30f --- /dev/null +++ b/docs/user/.envrc @@ -0,0 +1 @@ +use flake diff --git a/docs/user/.gitignore b/docs/user/.gitignore new file mode 100644 index 00000000..7585238e --- /dev/null +++ b/docs/user/.gitignore @@ -0,0 +1 @@ +book diff --git a/docs/user/book.toml b/docs/user/book.toml new file mode 100644 index 00000000..333659cb --- /dev/null +++ b/docs/user/book.toml @@ -0,0 +1,6 @@ +[book] +authors = ["The Aeneas contributors"] +language = "en" +multilingual = false +src = "src" +title = "Aeneas user documentation" diff --git a/docs/user/flake.lock b/docs/user/flake.lock new file mode 100644 index 00000000..dfd3938b --- /dev/null +++ b/docs/user/flake.lock @@ -0,0 +1,256 @@ +{ + "nodes": { + "alectryon": { + "flake": false, + "locked": { + "lastModified": 1654613606, + "narHash": "sha256-IGCn1PzTyw8rrwmyWUiw3Jo/dyZVGkMslnHYW7YB8yk=", + "owner": "Kha", + "repo": "alectryon", + "rev": "c3b16f650665745e1da4ddfcc048d3bd639f71d5", + "type": "github" + }, + "original": { + "owner": "Kha", + "ref": "typeid", + "repo": "alectryon", + "type": "github" + } + }, + "flake-compat": { + "flake": false, + "locked": { + "lastModified": 1673956053, + "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=", + "owner": "edolstra", + "repo": "flake-compat", + "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9", + "type": "github" + }, + "original": { + "owner": "edolstra", + "repo": "flake-compat", + "type": "github" + } + }, + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "lean": { + "inputs": { + "flake-utils": "flake-utils", + "lean4-mode": "lean4-mode", + "nix": "nix", + "nixpkgs": "nixpkgs_2", + "nixpkgs-old": "nixpkgs-old" + }, + "locked": { + "lastModified": 1720529829, + "narHash": "sha256-hPqn4qRfe7bLAaNRvK1RDC50IUuCaxDCcv5NtNsETEQ=", + "owner": "leanprover", + "repo": "lean4", + "rev": "f531f4e5db8f402a015a69373af9a002fe754acd", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "lean4", + "type": "github" + } + }, + "lean4-mode": { + "flake": false, + "locked": { + "lastModified": 1709737301, + "narHash": "sha256-uT9JN2kLNKJK9c/S/WxLjiHmwijq49EgLb+gJUSDpz0=", + "owner": "leanprover", + "repo": "lean4-mode", + "rev": "f1f24c15134dee3754b82c9d9924866fe6bc6b9f", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "lean4-mode", + "type": "github" + } + }, + "leanInk": { + "flake": false, + "locked": { + "lastModified": 1706870309, + "narHash": "sha256-5HhF/0mmPVvmcScE4t/UTB6IPuf050UJhNZprEQZ/aw=", + "owner": "leanprover", + "repo": "LeanInk", + "rev": "c54475dffc030aa67113eff600105b62eca646db", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "LeanInk", + "type": "github" + } + }, + "libgit2": { + "flake": false, + "locked": { + "lastModified": 1697646580, + "narHash": "sha256-oX4Z3S9WtJlwvj0uH9HlYcWv+x1hqp8mhXl7HsLu2f0=", + "owner": "libgit2", + "repo": "libgit2", + "rev": "45fd9ed7ae1a9b74b957ef4f337bc3c8b3df01b5", + "type": "github" + }, + "original": { + "owner": "libgit2", + "repo": "libgit2", + "type": "github" + } + }, + "mdBook": { + "flake": false, + "locked": { + "lastModified": 1660074464, + "narHash": "sha256-W30G7AeWBjdJE/CQZJU5vJjaDGZtpmxEKNMEvaYtuF8=", + "owner": "leanprover", + "repo": "mdBook", + "rev": "9321c10c502cd59eea8afc4325a84eab3ddf9391", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "mdBook", + "type": "github" + } + }, + "nix": { + "inputs": { + "flake-compat": "flake-compat", + "libgit2": "libgit2", + "nixpkgs": "nixpkgs", + "nixpkgs-regression": "nixpkgs-regression" + }, + "locked": { + "lastModified": 1711102798, + "narHash": "sha256-CXOIJr8byjolqG7eqCLa+Wfi7rah62VmLoqSXENaZnw=", + "owner": "NixOS", + "repo": "nix", + "rev": "a22328066416650471c3545b0b138669ea212ab4", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nix", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1709083642, + "narHash": "sha256-7kkJQd4rZ+vFrzWu8sTRtta5D1kBG0LSRYAfhtmMlSo=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "b550fe4b4776908ac2a861124307045f8e717c8e", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "release-23.11", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-old": { + "flake": false, + "locked": { + "lastModified": 1581379743, + "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-19.03", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-regression": { + "locked": { + "lastModified": 1643052045, + "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", + "type": "github" + } + }, + "nixpkgs_2": { + "locked": { + "lastModified": 1710889954, + "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixpkgs-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "alectryon": "alectryon", + "flake-utils": [ + "lean", + "flake-utils" + ], + "lean": "lean", + "leanInk": "leanInk", + "mdBook": "mdBook" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/docs/user/flake.nix b/docs/user/flake.nix new file mode 100644 index 00000000..be157614 --- /dev/null +++ b/docs/user/flake.nix @@ -0,0 +1,110 @@ +# Taken from Lean documentation's flake.nix +{ + description = "Aeneas documentation"; + + inputs.lean.url = "github:leanprover/lean4"; + inputs.flake-utils.follows = "lean/flake-utils"; + inputs.mdBook = { + url = "github:leanprover/mdBook"; + flake = false; + }; + inputs.alectryon = { + url = "github:Kha/alectryon/typeid"; + flake = false; + }; + inputs.leanInk = { + url = "github:leanprover/LeanInk"; + flake = false; + }; + + outputs = inputs@{ self, ... }: inputs.flake-utils.lib.eachDefaultSystem (system: + with inputs.lean.packages.${system}; with nixpkgs; + let + doc-src = ./.; # lib.sourceByRegex ../. ["doc.*" "tests(/lean(/beginEndAsMacro.lean)?)?"]; + in { + packages = rec { + lean-mdbook = mdbook.overrideAttrs (drv: rec { + name = "lean-${mdbook.name}"; + src = inputs.mdBook; + cargoDeps = drv.cargoDeps.overrideAttrs (_: { + inherit src; + outputHash = "sha256-CO3A9Kpp4sIvkT9X3p+GTidazk7Fn4jf0AP2PINN44A="; + }); + doCheck = false; + }); + book = stdenv.mkDerivation { + name = "aeneas-doc"; + src = doc-src; + buildInputs = [ lean-mdbook ]; + buildCommand = '' + mkdir $out + # necessary for `additional-css`...? + cp -vr --no-preserve=mode $src/* . + mdbook build -d $out + ''; + }; + # We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache + test = stdenv.mkDerivation { + name = "aeneas-doc-test"; + src = doc-src; + buildInputs = [ lean-mdbook stage1.Lean.lean-package strace ]; + patchPhase = '' + cd doc + patchShebangs test + ''; + buildPhase = '' + mdbook test + touch $out + ''; + dontInstall = true; + }; + + leanInk = (buildLeanPackage { + name = "Main"; + src = inputs.leanInk; + deps = [ (buildLeanPackage { + name = "LeanInk"; + src = inputs.leanInk; + }) ]; + executableName = "leanInk"; + linkFlags = ["-rdynamic"]; + }).executable; + + alectryon = python3Packages.buildPythonApplication { + name = "alectryon"; + src = inputs.alectryon; + propagatedBuildInputs = + [ leanInk lean-all ] ++ + # https://github.com/cpitclaudel/alectryon/blob/master/setup.cfg + (with python3Packages; [ pygments dominate beautifulsoup4 docutils ]); + doCheck = false; + }; + + renderLeanMod = mod: mod.overrideAttrs (final: prev: { + name = "${prev.name}.md"; + buildInputs = prev.buildInputs ++ [ alectryon ]; + outputs = [ "out" ]; + buildCommand = '' + dir=$(dirname $relpath) + mkdir -p $dir out/$dir + if [ -d $src ]; then cp -r $src/. $dir/; else cp $src $leanPath; fi + alectryon --frontend lean4+markup $leanPath --backend webpage -o $out/$leanPath.md + ''; + }); + + renderPackage = pkg: symlinkJoin { + name = "${pkg.name}-mds"; + paths = map renderLeanMod (lib.attrValues pkg.mods); + }; + + literate = buildLeanPackage { + name = "literate"; + src = ./.; + roots = [ ]; + }; + inked = renderPackage literate; + doc = book; + }; + defaultPackage = self.packages.${system}.doc; + }); +} diff --git a/docs/user/src/README.md b/docs/user/src/README.md new file mode 100644 index 00000000..fa1cac5c --- /dev/null +++ b/docs/user/src/README.md @@ -0,0 +1,16 @@ +# Introduction to Aeneas + +Aeneas is a verification toolchain for Rust programs aiming to embed purely functional translation of Rust programs into theorem provers such as Coq or Lean. + +## What it can do? + +Aeneas aims to provide verification facilities for **safe** Rust with some caveats described in the next section. + +## What it cannot do? + +- loops: no nested loops for now. We are working on lifting this limitation. +- no functions pointers/closures: ongoing work. We have support for traits and will have support for function pointers and closures soon. +- limited type parametricity: it is not possible for now to instantiate a type parameter with a type containing a borrow. This is mostly an engineering issue. +- no nested borrows in function signatures: ongoing work. +- interior mutability: ongoing work. We are thinking of modeling the effects of interior mutability by using ghost states. +- no concurrent execution: long-term effort. We plan to address coarse-grained parallelism as a long-term goal. diff --git a/docs/user/src/SUMMARY.md b/docs/user/src/SUMMARY.md new file mode 100644 index 00000000..54a6905b --- /dev/null +++ b/docs/user/src/SUMMARY.md @@ -0,0 +1,11 @@ +# Summary + +[Introduction](./README.md) + +# Setup guide + +# Proving with Lean + +## Tactics guide + +- [Progress](./lean/tactics/progress.md) diff --git a/docs/user/src/lean/tactics/progress.md b/docs/user/src/lean/tactics/progress.md new file mode 100644 index 00000000..4617ec6c --- /dev/null +++ b/docs/user/src/lean/tactics/progress.md @@ -0,0 +1,2 @@ +# Progress +