Merge branch 'main' into core-fmt

.utils/expand.sh

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+# This script expands a crate so that one can inspect macro expansion
+# by hax. It is a wrapper around `cargo expand` that inject the
+# required rustc flags.
+
+RUSTFLAGS='-Zcrate-attr=register_tool(_hax) -Zcrate-attr=feature(register_tool) --cfg hax_compilation --cfg _hax --cfg hax --cfg hax_backend_fstar --cfg hax' cargo expand "$@"
+

engine/backends/coq/coq/coq_backend.ml

@@ -43,7 +43,8 @@ module SubtypeToInputLanguage
              and type state_passing_loop = Features.Off.state_passing_loop
              and type dyn = Features.Off.dyn
              and type match_guard = Features.Off.match_guard
-             and type trait_item_default = Features.Off.trait_item_default) =
+             and type trait_item_default = Features.Off.trait_item_default
+             and type unsafe = Features.Off.unsafe) =
 struct
   module FB = InputLanguage
 
@@ -701,7 +702,8 @@ open Phase_utils
 
 module TransformToInputLanguage =
   [%functor_application
-  Phases.Reject.RawOrMutPointer(Features.Rust)
+  Phases.Reject.Unsafe(Features.Rust)
+  |> Phases.Reject.RawOrMutPointer
   |> Phases.And_mut_defsite
   |> Phases.Reconstruct_asserts
   |> Phases.Reconstruct_for_loops

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -43,7 +43,8 @@ module SubtypeToInputLanguage
              and type block = Features.Off.block
              and type dyn = Features.Off.dyn
              and type match_guard = Features.Off.match_guard
-             and type trait_item_default = Features.Off.trait_item_default) =
+             and type trait_item_default = Features.Off.trait_item_default
+             and type unsafe = Features.Off.unsafe) =
 struct
   module FB = InputLanguage
 
@@ -565,7 +566,8 @@ open Phase_utils
 
 module TransformToInputLanguage (* : PHASE *) =
   [%functor_application
-    Phases.Reject.RawOrMutPointer(Features.Rust)
+    Phases.Reject.Unsafe(Features.Rust)
+    |> Phases.Reject.RawOrMutPointer
     |> Phases.And_mut_defsite
     |> Phases.Reconstruct_asserts
     |> Phases.Reconstruct_for_loops

engine/backends/easycrypt/easycrypt_backend.ml

@@ -61,6 +61,7 @@ module RejectNotEC (FA : Features.T) = struct
         let dyn = reject
         let match_guard = reject
         let trait_item_default = reject
+        let unsafe = reject
         let construct_base _ _ = Features.On.construct_base
         let for_index_loop _ _ = Features.On.for_index_loop
 
@@ -347,10 +348,10 @@ open Phase_utils
 
 module TransformToInputLanguage =
 [%functor_application
-Phases.Reject.RawOrMutPointer Features.Rust |> Phases.And_mut_defsite
-|> Phases.Reconstruct_asserts |> Phases.Reconstruct_for_loops
-|> Phases.Direct_and_mut |> Phases.Drop_blocks |> Phases.Reject.Continue
-|> Phases.Drop_references |> RejectNotEC]
+Phases.Reject.RawOrMutPointer Features.Rust |> Phases.Reject.Unsafe
+|> Phases.And_mut_defsite |> Phases.Reconstruct_asserts
+|> Phases.Reconstruct_for_loops |> Phases.Direct_and_mut |> Phases.Drop_blocks
+|> Phases.Reject.Continue |> Phases.Drop_references |> RejectNotEC]
 
 let apply_phases (_bo : BackendOptions.t) (items : Ast.Rust.item list) :
     AST.item list =

engine/backends/fstar/fstar_backend.ml

@@ -42,7 +42,8 @@ module SubtypeToInputLanguage
              and type for_index_loop = Features.Off.for_index_loop
              and type state_passing_loop = Features.Off.state_passing_loop
              and type match_guard = Features.Off.match_guard
-             and type trait_item_default = Features.Off.trait_item_default) =
+             and type trait_item_default = Features.Off.trait_item_default
+             and type unsafe = Features.Off.unsafe) =
 struct
   module FB = InputLanguage
 
@@ -1683,7 +1684,8 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 
 module TransformToInputLanguage =
   [%functor_application
-  Phases.Reject.RawOrMutPointer(Features.Rust)
+  Phases.Reject.Unsafe(Features.Rust)
+  |> Phases.Reject.RawOrMutPointer
   |> Phases.Transform_hax_lib_inline
   |> Phases.Specialize
   |> Phases.Drop_sized_trait

engine/backends/proverif/proverif_backend.ml

@@ -79,6 +79,7 @@ struct
         let dyn = reject
         let match_guard = reject
         let trait_item_default = reject
+        let unsafe = reject
         let metadata = Phase_reject.make_metadata (NotInBackendLang ProVerif)
       end)
 
@@ -888,11 +889,12 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 
 module TransformToInputLanguage =
   [%functor_application
-    Phases.Reject.RawOrMutPointer(Features.Rust)
-    |> Phases.Transform_hax_lib_inline
-    |> Phases.Simplify_question_marks
-    |> Phases.And_mut_defsite
-    |> Phases.Reconstruct_for_loops
+  Phases.Reject.Unsafe(Features.Rust)
+  |> Phases.Reject.RawOrMutPointer
+  |> Phases.Transform_hax_lib_inline
+  |> Phases.Simplify_question_marks
+  |> Phases.And_mut_defsite
+  |> Phases.Reconstruct_for_loops
   |> Phases.Direct_and_mut
   |> Phases.Reject.Arbitrary_lhs
   |> Phases.Drop_blocks

engine/lib/ast.ml

@@ -105,6 +105,9 @@ functor
   (F : Features.T)
   ->
   struct
+    type safety_kind = Safe | Unsafe of F.unsafe
+    [@@deriving show, yojson, hash, eq]
+
     type borrow_kind = Shared | Unique | Mut of F.mutable_reference
     [@@deriving show, yojson, hash, eq]
 
@@ -240,7 +243,7 @@ functor
           rhs : expr;
           body : expr;
         }
-      | Block of (expr * F.block)
+      | Block of { e : expr; safety_mode : safety_kind; witness : F.block }
         (* Corresponds to `{e}`: this is important for places *)
       | LocalVar of local_ident
       | GlobalVar of global_ident
@@ -391,6 +394,7 @@ functor
           generics : generics;
           body : expr;
           params : param list;
+          safety : safety_kind;
         }
       | TyAlias of { name : concrete_ident; generics : generics; ty : ty }
       | Type of {
@@ -409,13 +413,15 @@ functor
           name : concrete_ident;
           generics : generics;
           items : trait_item list;
+          safety : safety_kind;
         }
       | Impl of {
           generics : generics;
           self_ty : ty;
           of_trait : global_ident * generic_value list;
           items : impl_item list;
           parent_bounds : (impl_expr * impl_ident) list;
+          safety : safety_kind;
         }
       | Alias of { name : concrete_ident; item : concrete_ident }
           (** `Alias {name; item}` is basically a `use

engine/lib/ast_utils.ml

@@ -58,7 +58,7 @@ module Make (F : Features.T) = struct
       match e.e with Borrow { e; _ } -> Some e | _ -> None
 
     let block (e : expr) : expr option =
-      match e.e with Block (e, _) -> Some e | _ -> None
+      match e.e with Block { e; _ } -> Some e | _ -> None
 
     let deref (e : expr) : expr option =
       match e.e with
@@ -173,7 +173,8 @@ module Make (F : Features.T) = struct
 
   let functions_of_item (x : item) : (concrete_ident * expr) list =
     match x.v with
-    | Fn { name; generics = _; body; params = _ } -> [ (name, body) ]
+    | Fn { name; generics = _; body; params = _; safety = _ } ->
+        [ (name, body) ]
     | Impl { items; _ } ->
         List.filter_map
           ~f:(fun w ->
@@ -252,13 +253,14 @@ module Make (F : Features.T) = struct
 
         method! visit_item' () item' =
           match item' with
-          | Fn { name; generics; body; params } ->
+          | Fn { name; generics; body; params; safety } ->
               Fn
                 {
                   name;
                   generics;
                   body = { body with e = GlobalVar (`TupleCons 0) };
                   params;
+                  safety;
                 }
           | _ -> super#visit_item' () item'
       end

engine/lib/attr_payloads.ml

@@ -161,10 +161,6 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
     val expect_expr :
       ?keep_last_args:int -> generics * param list * expr -> expr
 
-    val associated_expr_rebinding :
-      span -> pat list -> AssocRole.t -> attrs -> expr option
-    (** Looks up an expression but takes care of rebinding free variables. *)
-
     val associated_refinement_in_type :
       span -> string list -> attrs -> expr option
     (** For type, there is a special treatment. The name of fields are
@@ -277,55 +273,6 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
         attrs -> expr list =
       associated_fns role >> List.map ~f:(expect_expr ~keep_last_args)
 
-    let associated_expr_rebinding span (params : pat list) (role : AssocRole.t)
-        (attrs : attrs) : expr option =
-      let* _, original_params, body = associated_fn role attrs in
-      let original_params =
-        List.map ~f:(fun param -> param.pat) original_params
-      in
-      let vars_of_pat =
-        U.Reducers.collect_local_idents#visit_pat () >> Set.to_list
-      in
-      let original_vars = List.concat_map ~f:vars_of_pat original_params in
-      let target_vars = List.concat_map ~f:vars_of_pat params in
-      let mk_error_message prefix =
-        prefix ^ "\n" ^ "\n - original_vars: "
-        ^ [%show: local_ident list] original_vars
-        ^ "\n - target_vars: "
-        ^ [%show: local_ident list] target_vars
-        ^ "\n\n - original_params: "
-        ^ [%show: pat list] original_params
-        ^ "\n - params: "
-        ^ [%show: pat list] params
-      in
-      let replacements =
-        List.zip_opt original_vars target_vars
-        |> Option.value_or_thunk ~default:(fun _ ->
-               let details =
-                 mk_error_message
-                   "associated_expr_rebinding: zip two lists of different \
-                    lengths (original_vars and target_vars)"
-               in
-               Error.unimplemented ~details span)
-      in
-      let replacements =
-        match Map.of_alist (module Local_ident) replacements with
-        | `Ok replacements -> replacements
-        | `Duplicate_key key ->
-            let details =
-              mk_error_message
-                "associated_expr_rebinding: of_alist failed because `"
-              ^ [%show: local_ident] key
-              ^ "` is a duplicate key. Context: "
-            in
-            Error.unimplemented ~details span
-      in
-      Some
-        ((U.Mappers.rename_local_idents (fun v ->
-              Map.find replacements v |> Option.value ~default:v))
-           #visit_expr
-           () body)
-
     let associated_refinement_in_type span (free_variables : string list) :
         attrs -> expr option =
       associated_fn Refine

engine/lib/dependencies.ml

@@ -39,7 +39,7 @@ module Make (F : Features.T) = struct
       in
       let set =
         match i.v with
-        | Fn { name = _; generics; body; params } ->
+        | Fn { name = _; generics; body; params; _ } ->
             v#visit_generics () generics
             @ v#visit_expr () body
             @ concat_map (v#visit_param ()) params
@@ -51,10 +51,11 @@ module Make (F : Features.T) = struct
         | IMacroInvokation { macro; argument = (_ : string); span; witness = _ }
           ->
             v#visit_concrete_ident () macro @ v#visit_span () span
-        | Trait { name = _; generics; items } ->
+        | Trait { name = _; generics; items; safety = _ } ->
             v#visit_generics () generics
             @ concat_map (v#visit_trait_item ()) items
-        | Impl { generics; self_ty; of_trait; items; parent_bounds } ->
+        | Impl { generics; self_ty; of_trait; items; parent_bounds; safety = _ }
+          ->
             v#visit_generics () generics
             @ v#visit_ty () self_ty
             @ v#visit_global_ident () (fst of_trait)

engine/lib/diagnostics.ml

@@ -17,6 +17,7 @@ module Phase = struct
       | AsPattern
       | Dyn
       | TraitItemDefault
+      | Unsafe
     [@@deriving show { with_path = false }, eq, yojson, compare, hash, sexp]
 
     let display = function

engine/lib/features.ml

@@ -26,7 +26,8 @@ loop,
   block,
   dyn,
   match_guard,
-  trait_item_default]
+  trait_item_default,
+  unsafe]
 
 module Full = On
 

engine/lib/generic_printer/generic_printer.ml

@@ -186,7 +186,11 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
                   ~lhs ~rhs body
                 |> wrap_parens
             | Literal l -> print#literal Expr l
-            | Block (e, _) -> print#expr ctx e
+            | Block { e; safety_mode; _ } -> (
+                let e = lbrace ^/^ nest 2 (print#expr ctx e) ^/^ rbrace in
+                match safety_mode with
+                | Safe -> e
+                | Unsafe _ -> !^"unsafe " ^^ e)
             | Array l ->
                 separate_map comma (print#expr_at Expr_Array) l
                 |> group |> brackets
@@ -388,13 +392,19 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
 
         method item' : item' fn =
           function
-          | Fn { name; generics; body; params } ->
+          | Fn { name; generics; body; params; safety } ->
               let params =
                 iblock parens
                   (separate_map (comma ^^ break 1) print#param params)
               in
               let generics = print#generic_params generics.params in
-              string "fn" ^^ space ^^ print#concrete_ident name ^^ generics
+              let safety =
+                optional Base.Fn.id
+                  (match safety with
+                  | Safe -> None
+                  | Unsafe _ -> Some !^"unsafe ")
+              in
+              safety ^^ !^"fn" ^^ space ^^ print#concrete_ident name ^^ generics
               ^^ params
               ^^ iblock braces (print#expr_at Item_Fn_body body)
           | Quote quote -> print#quote quote