summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/Assumed.ml1
-rw-r--r--compiler/Extract.ml5
-rw-r--r--compiler/ExtractBase.ml5
-rw-r--r--compiler/InterpreterExpansion.ml3
-rw-r--r--compiler/Print.ml30
-rw-r--r--compiler/PrintPure.ml8
-rw-r--r--compiler/Pure.ml18
-rw-r--r--compiler/PureTypeCheck.ml2
-rw-r--r--compiler/SymbolicToPure.ml13
-rw-r--r--compiler/SynthesizeSymbolic.ml4
-rw-r--r--compiler/TypesAnalysis.ml3
-rw-r--r--compiler/dune2
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)))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 18:22:29 +0000