Update following the addition of raw pointers

12 files changed, 77 insertions, 17 deletions

diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index 94fb7a72..79f6b0d4 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -85,6 +85,7 @@ module Sig = struct
       { regions_outlive = []; types_outlive = []; trait_type_constraints = [] }
     in
     {
+      is_unsafe = false;
       generics;
       preds;
       parent_params_info = None;
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 91827a31..afd722e5 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -64,7 +64,9 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
     | BitAnd -> "and"
     | BitOr -> "or"
     | Shl -> "lsl"
-    | Shr -> "asr" (* NOTE: make sure arithmetic shift right is implemented, i.e. OCaml's asr operator, not lsr *)
+    | Shr ->
+        "asr"
+        (* NOTE: make sure arithmetic shift right is implemented, i.e. OCaml's asr operator, not lsr *)
     | _ -> raise (Failure "Unreachable")
   in
   (* Remark: the Lean case is actually not used *)
@@ -798,6 +800,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
             | Assumed Slice -> "s"
             | Assumed Str -> "s"
             | Assumed State -> ConstStrings.state_basename
+            | Assumed (RawPtr _) -> "p"
             | AdtId adt_id ->
                 let def = TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls in
                 (* Derive the var name from the last ident of the type name
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 8f32ba44..3eef6b3b 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -758,7 +758,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
             if variant_id = fuel_zero_id then "@fuel::0"
             else if variant_id = fuel_succ_id then "@fuel::Succ"
             else raise (Failure "Unreachable")
-        | Assumed (State | Array | Slice | Str) ->
+        | Assumed (State | Array | Slice | Str | RawPtr _) ->
             raise
               (Failure
                  ("Unreachable: variant id ("
@@ -777,7 +777,8 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
       let field_name =
         match id with
         | Tuple -> raise (Failure "Unreachable")
-        | Assumed (State | Result | Error | Fuel | Array | Slice | Str) ->
+        | Assumed
+            (State | Result | Error | Fuel | Array | Slice | Str | RawPtr _) ->
             (* We can't directly have access to the fields of those types *)
             raise (Failure "Unreachable")
         | AdtId id -> (
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 167e3d58..b267bb51 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -696,7 +696,8 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
             raise
               (Failure
                  "Attempted to greedily expand an ADT which can't be expanded ")
-        | T.TypeVar _ | T.Literal _ | Never | T.TraitType _ | T.Arrow _ ->
+        | T.TypeVar _ | T.Literal _ | Never | T.TraitType _ | T.Arrow _
+        | T.RawPtr _ ->
             raise (Failure "Unreachable")
       in
       (* Compose and continue *)
diff --git a/compiler/Print.ml b/compiler/Print.ml
index aeacfbf0..7f0d95ff 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -660,6 +660,30 @@ module EvalCtxLlbcAst = struct
     let fmt = PC.ctx_to_stype_formatter fmt in
     PT.sty_to_string fmt t
 
+  let generic_params_to_strings (ctx : C.eval_ctx) (x : T.generic_params) :
+      string list * string list =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_stype_formatter fmt in
+    PT.generic_params_to_strings fmt x
+
+  let egeneric_args_to_string (ctx : C.eval_ctx) (x : T.egeneric_args) : string
+      =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_etype_formatter fmt in
+    PT.egeneric_args_to_string fmt x
+
+  let rgeneric_args_to_string (ctx : C.eval_ctx) (x : T.rgeneric_args) : string
+      =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_rtype_formatter fmt in
+    PT.rgeneric_args_to_string fmt x
+
+  let sgeneric_args_to_string (ctx : C.eval_ctx) (x : T.sgeneric_args) : string
+      =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_stype_formatter fmt in
+    PT.sgeneric_args_to_string fmt x
+
   let etrait_ref_to_string (ctx : C.eval_ctx) (x : T.etrait_ref) : string =
     let fmt = PC.eval_ctx_to_ctx_formatter ctx in
     let fmt = PC.ctx_to_etype_formatter fmt in
@@ -693,12 +717,6 @@ module EvalCtxLlbcAst = struct
     let fmt = PC.ctx_to_stype_formatter fmt in
     PT.strait_instance_id_to_string fmt x
 
-  let egeneric_args_to_string (ctx : C.eval_ctx) (x : T.egeneric_args) : string
-      =
-    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
-    let fmt = PC.ctx_to_etype_formatter fmt in
-    PT.egeneric_args_to_string fmt x
-
   let borrow_content_to_string (ctx : C.eval_ctx) (bc : V.borrow_content) :
       string =
     let fmt = PC.eval_ctx_to_ctx_formatter ctx in
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 6396fe96..ec75fcfd 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -198,6 +198,8 @@ let assumed_ty_to_string (aty : assumed_ty) : string =
   | Array -> "Array"
   | Slice -> "Slice"
   | Str -> "Str"
+  | RawPtr Mut -> "MutRawPtr"
+  | RawPtr Const -> "ConstRawPtr"
 
 let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
   match id with
@@ -385,7 +387,7 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
   | Assumed aty -> (
       (* Assumed type *)
       match aty with
-      | State | Array | Slice | Str ->
+      | State | Array | Slice | Str | RawPtr _ ->
           (* Those types are opaque: we can't get there *)
           raise (Failure "Unreachable")
       | Result ->
@@ -423,7 +425,7 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
       | State | Fuel | Array | Slice | Str ->
           (* Opaque types: we can't get there *)
           raise (Failure "Unreachable")
-      | Result | Error ->
+      | Result | Error | RawPtr _ ->
           (* Enumerations: we can't get there *)
           raise (Failure "Unreachable"))
 
@@ -463,7 +465,7 @@ let adt_g_value_to_string (fmt : value_formatter)
   | Adt (Assumed aty, _) -> (
       (* Assumed type *)
       match aty with
-      | State ->
+      | State | RawPtr _ ->
           (* This type is opaque: we can't get there *)
           raise (Failure "Unreachable")
       | Result ->
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 81e13af7..9a3654b8 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -47,6 +47,7 @@ type trait_clause_id = T.trait_clause_id [@@deriving show, ord]
 type trait_item_name = T.trait_item_name [@@deriving show, ord]
 type global_decl_id = T.global_decl_id [@@deriving show, ord]
 type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
+type mutability = Mut | Const [@@deriving show, ord]
 
 (** The assumed types for the pure AST.
 
@@ -64,7 +65,22 @@ type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
         this state is opaque to Aeneas (the user can define it, or leave it as
         assumed)
   *)
-type assumed_ty = State | Result | Error | Fuel | Array | Slice | Str
+type assumed_ty =
+  | State
+  | Result
+  | Error
+  | Fuel
+  | Array
+  | Slice
+  | Str
+  | RawPtr of mutability
+      (** The bool
+          Raw pointers don't make sense in the pure world, but we don't know
+          how to translate them yet and we have to handle some functions which
+          use raw pointers in their signature (for instance some trait declarations
+          for the slices). For now, we use a dedicated type to "mark" the raw pointers,
+          and make sure that those functions are actually not used in the translation.
+       *)
 [@@deriving show, ord]
 
 (* TODO: we should never directly manipulate [Return] and [Fail], but rather
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index d31f0cf9..2ad942bb 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -46,7 +46,7 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
           if variant_id = fuel_zero_id then []
           else if variant_id = fuel_succ_id then [ mk_fuel_ty ]
           else raise (Failure "Unreachable: improper variant id for fuel type")
-      | Array | Slice | Str ->
+      | Array | Slice | Str | RawPtr _ ->
           (* Array: when not symbolic values (for instance, because of aggregates),
              the array expressions are introduced as struct updates *)
           raise (Failure "Attempting to access the fields of an opaque type"))
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 9c698b51..4ba5296f 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -421,6 +421,11 @@ let rec translate_sty (ty : T.sty) : ty =
   | Literal ty -> Literal ty
   | Never -> raise (Failure "Unreachable")
   | Ref (_, rty, _) -> translate rty
+  | RawPtr (ty, rkind) ->
+      let mut = match rkind with Mut -> Mut | Shared -> Const in
+      let ty = translate ty in
+      let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
+      Adt (Assumed (RawPtr mut), generics)
   | TraitType (trait_ref, generics, type_name) ->
       let trait_ref = translate_strait_ref trait_ref in
       let generics = translate_sgeneric_args generics in
@@ -560,6 +565,11 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
   | Never -> raise (Failure "Unreachable")
   | Literal lty -> Literal lty
   | Ref (_, rty, _) -> translate rty
+  | RawPtr (ty, rkind) ->
+      let mut = match rkind with Mut -> Mut | Shared -> Const in
+      let ty = translate ty in
+      let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
+      Adt (Assumed (RawPtr mut), generics)
   | TraitType (trait_ref, generics, type_name) ->
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
       let generics = translate_fwd_generic_args type_infos generics in
@@ -646,6 +656,9 @@ let rec translate_back_ty (type_infos : TA.type_infos)
           if keep_region r then
             translate_back_ty type_infos keep_region inside_mut rty
           else None)
+  | RawPtr _ ->
+      (* TODO: not sure what to do here *)
+      None
   | TraitType (trait_ref, generics, type_name) ->
       assert (generics.regions = []);
       (* Translate the trait ref and the generics as "forward" generics -
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 9084f2b3..9dd65c84 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -85,7 +85,9 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
             match ls with
             | [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
             | _ -> raise (Failure "Ill-formed borrow expansion"))
-        | T.TypeVar _ | T.Literal Char | Never | T.TraitType _ | T.Arrow _ ->
+        | T.TypeVar _
+        | T.Literal Char
+        | Never | T.TraitType _ | T.Arrow _ | T.RawPtr _ ->
             raise (Failure "Ill-formed symbolic expansion")
       in
       Some (Expansion (place, sv, expansion))
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 16f8c5f9..38d350b1 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -168,6 +168,9 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
         in
         (* Continue exploring *)
         analyze expl_info ty_info rty
+    | RawPtr (rty, _) ->
+        (* TODO: not sure what to do here *)
+        analyze expl_info ty_info rty
     | Adt ((Tuple | Assumed (Box | Slice | Array | Str)), generics) ->
         (* Nothing to update: just explore the type parameters *)
         List.fold_left
diff --git a/compiler/dune b/compiler/dune
index 4ec46b70..a4b09df4 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -92,4 +92,4 @@
    -g
    ;-dsource
    -warn-error
-   -5-8-9-11-14-33-20-21-26-27-39)))
+   -5@8-9-11-14-33-20-21-26-27-39)))