summaryrefslogtreecommitdiff
path: root/compiler/SymbolicToPure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/SymbolicToPure.ml')
-rw-r--r--compiler/SymbolicToPure.ml214
1 files changed, 107 insertions, 107 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 922aa307..2460e040 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2,18 +2,19 @@ open Utils
open LlbcAstUtils
open Pure
open PureUtils
+open PrimitiveValues
+module T = Types
module Id = Identifiers
module C = Contexts
module A = LlbcAst
module S = SymbolicAst
module TA = TypesAnalysis
-module L = Logging
module PP = PrintPure
module FA = FunsAnalysis
module IU = InterpreterUtils
(** The local logger *)
-let log = L.symbolic_to_pure_log
+let log = Logging.symbolic_to_pure_log
type type_context = {
llbc_type_decls : T.type_decl TypeDeclId.Map.t;
@@ -208,113 +209,92 @@ type bs_ctx = {
[@@deriving show]
(* TODO: move *)
-let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter =
- Print.Ast.decls_and_fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls
- ctx.fun_context.llbc_fun_decls ctx.global_context.llbc_global_decls
- ctx.trait_decls_ctx ctx.trait_impls_ctx ctx.fun_decl
-
-let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter =
- let region_id_to_string = Print.Types.region_id_to_string in
- let type_var_id_to_string = Print.Types.type_var_id_to_string in
- let var_id_to_string = Print.Expressions.var_id_to_string in
- let ast_fmt = bs_ctx_to_ast_formatter ctx in
+let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env =
+ let type_decls = ctx.type_context.llbc_type_decls in
+ let fun_decls = ctx.fun_context.llbc_fun_decls in
+ let global_decls = ctx.global_context.llbc_global_decls in
+ let trait_decls = ctx.trait_decls_ctx in
+ let trait_impls = ctx.trait_impls_ctx in
+ let generics = ctx.fun_decl.signature.generics in
+ let preds = ctx.fun_decl.signature.preds in
{
- Print.Values.region_id_to_string;
- type_var_id_to_string;
- type_decl_id_to_string = ast_fmt.type_decl_id_to_string;
- const_generic_var_id_to_string = ast_fmt.const_generic_var_id_to_string;
- global_decl_id_to_string = ast_fmt.global_decl_id_to_string;
- adt_variant_to_string = ast_fmt.adt_variant_to_string;
- var_id_to_string;
- adt_field_names = ast_fmt.adt_field_names;
- trait_decl_id_to_string = ast_fmt.trait_decl_id_to_string;
- trait_impl_id_to_string = ast_fmt.trait_impl_id_to_string;
- trait_clause_id_to_string = ast_fmt.trait_clause_id_to_string;
+ type_decls;
+ fun_decls;
+ global_decls;
+ trait_decls;
+ trait_impls;
+ generics;
+ preds;
+ locals = [];
}
-let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
- let generics = ctx.fun_decl.signature.generics in
+let bs_ctx_to_pure_fmt_env (ctx : bs_ctx) : PrintPure.fmt_env =
let type_decls = ctx.type_context.llbc_type_decls in
let fun_decls = ctx.fun_context.llbc_fun_decls in
let global_decls = ctx.global_context.llbc_global_decls in
- PrintPure.mk_ast_formatter type_decls fun_decls global_decls
- ctx.trait_decls_ctx ctx.trait_impls_ctx generics.types
- generics.const_generics
+ let trait_decls = ctx.trait_decls_ctx in
+ let trait_impls = ctx.trait_impls_ctx in
+ let generics = ctx.sg.generics in
+ {
+ type_decls;
+ fun_decls;
+ global_decls;
+ trait_decls;
+ trait_impls;
+ generics;
+ locals = [];
+ }
let ctx_generic_args_to_string (ctx : bs_ctx) (args : T.generic_args) : string =
- let fmt = bs_ctx_to_ctx_formatter ctx in
- let fmt = Print.PC.ctx_to_type_formatter fmt in
- Print.PT.generic_args_to_string fmt args
+ let env = bs_ctx_to_fmt_env ctx in
+ Print.Types.generic_args_to_string env args
+
+let name_to_string (ctx : bs_ctx) =
+ Print.Types.name_to_string (bs_ctx_to_fmt_env ctx)
let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
- let fmt = bs_ctx_to_ctx_formatter ctx in
- let fmt = Print.PC.ctx_to_type_formatter fmt in
- Print.PV.symbolic_value_to_string fmt sv
+ let env = bs_ctx_to_fmt_env ctx in
+ Print.Values.symbolic_value_to_string env sv
let typed_value_to_string (ctx : bs_ctx) (v : V.typed_value) : string =
- let fmt = bs_ctx_to_ctx_formatter ctx in
- Print.PV.typed_value_to_string fmt v
+ let env = bs_ctx_to_fmt_env ctx in
+ Print.Values.typed_value_to_string env v
let pure_ty_to_string (ctx : bs_ctx) (ty : ty) : string =
- let fmt = bs_ctx_to_pp_ast_formatter ctx in
- let fmt = PrintPure.ast_to_type_formatter fmt in
- PrintPure.ty_to_string fmt false ty
+ let env = bs_ctx_to_pure_fmt_env ctx in
+ PrintPure.ty_to_string env false ty
let ty_to_string (ctx : bs_ctx) (ty : T.ty) : string =
- let fmt = bs_ctx_to_ctx_formatter ctx in
- let fmt = Print.PC.ctx_to_type_formatter fmt in
- Print.PT.ty_to_string fmt ty
+ let env = bs_ctx_to_fmt_env ctx in
+ Print.Types.ty_to_string env ty
let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
- let type_decls = ctx.type_context.llbc_type_decls in
- let global_decls = ctx.global_context.llbc_global_decls in
- let fmt =
- PrintPure.mk_type_formatter type_decls global_decls ctx.trait_decls_ctx
- ctx.trait_impls_ctx def.generics.types def.generics.const_generics
- in
- PrintPure.type_decl_to_string fmt def
+ let env = bs_ctx_to_pure_fmt_env ctx in
+ PrintPure.type_decl_to_string env def
let texpression_to_string (ctx : bs_ctx) (e : texpression) : string =
- let fmt = bs_ctx_to_pp_ast_formatter ctx in
- PrintPure.texpression_to_string fmt false "" " " e
+ let env = bs_ctx_to_pure_fmt_env ctx in
+ PrintPure.texpression_to_string env false "" " " e
let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
- let type_params = sg.generics.types in
- let cg_params = sg.generics.const_generics in
- let type_decls = ctx.type_context.llbc_type_decls in
- let fun_decls = ctx.fun_context.llbc_fun_decls in
- let global_decls = ctx.global_context.llbc_global_decls in
- let fmt =
- PrintPure.mk_ast_formatter type_decls fun_decls global_decls
- ctx.trait_decls_ctx ctx.trait_impls_ctx type_params cg_params
- in
- PrintPure.fun_sig_to_string fmt sg
+ let env = bs_ctx_to_pure_fmt_env ctx in
+ PrintPure.fun_sig_to_string env sg
let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
- let generics = def.signature.generics in
- let type_params = generics.types in
- let cg_params = generics.const_generics in
- let type_decls = ctx.type_context.llbc_type_decls in
- let fun_decls = ctx.fun_context.llbc_fun_decls in
- let global_decls = ctx.global_context.llbc_global_decls in
- let fmt =
- PrintPure.mk_ast_formatter type_decls fun_decls global_decls
- ctx.trait_decls_ctx ctx.trait_impls_ctx type_params cg_params
- in
- PrintPure.fun_decl_to_string fmt def
+ let env = bs_ctx_to_pure_fmt_env ctx in
+ PrintPure.fun_decl_to_string env def
let typed_pattern_to_string (ctx : bs_ctx) (p : Pure.typed_pattern) : string =
- let fmt = bs_ctx_to_pp_ast_formatter ctx in
- PrintPure.typed_pattern_to_string fmt p
+ let env = bs_ctx_to_pure_fmt_env ctx in
+ PrintPure.typed_pattern_to_string env p
(* TODO: move *)
let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
- let fmt = bs_ctx_to_ast_formatter ctx in
- let fmt = Print.Contexts.ast_to_value_formatter fmt in
+ let env = bs_ctx_to_fmt_env ctx in
let verbose = false in
let indent = "" in
let indent_incr = " " in
- Print.Values.abs_to_string fmt verbose indent indent_incr abs
+ Print.Values.abs_to_string env verbose indent indent_incr abs
let get_instantiated_fun_sig (fun_id : A.fun_id)
(back_id : T.RegionGroupId.id option) (generics : generic_args)
@@ -421,7 +401,7 @@ let rec translate_sty (ty : T.ty) : ty =
| TNever -> raise (Failure "Unreachable")
| TRef (_, rty, _) -> translate rty
| TRawPtr (ty, rkind) ->
- let mut = match rkind with Mut -> Mut | Shared -> 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)
@@ -481,21 +461,24 @@ let translate_variant (v : T.variant) : variant =
let translate_variants (vl : T.variant list) : variant list =
List.map translate_variant vl
-(** Translate a type def kind to IM *)
+(** Translate a type def kind from LLBC *)
let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind =
match kind with
| T.Struct fields -> Struct (translate_fields fields)
| T.Enum variants -> Enum (translate_variants variants)
| T.Opaque -> Opaque
-(** Translate a type definition from IM
+(** Translate a type definition from LLBC
- TODO: this is not symbolic to pure but IM to pure. Still, I don't see the
- point of moving this definition for now.
+ Remark: this is not symbolic to pure but LLBC to pure. Still,
+ I don't see the point of moving this definition for now.
*)
-let translate_type_decl (def : T.type_decl) : type_decl =
+let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
+ type_decl =
+ let env = Print.Contexts.decls_ctx_to_fmt_env ctx in
let def_id = def.T.def_id in
- let name = def.name in
+ let llbc_name = def.name in
+ let name = Print.Types.name_to_string env def.name in
let { T.regions; types; const_generics; trait_clauses } = def.generics in
(* Can't translate types with regions for now *)
assert (regions = []);
@@ -503,7 +486,7 @@ let translate_type_decl (def : T.type_decl) : type_decl =
let generics = { types; const_generics; trait_clauses } in
let kind = translate_type_decl_kind def.T.kind in
let preds = translate_predicates def.preds in
- { def_id; name; generics; kind; preds }
+ { def_id; llbc_name; name; generics; kind; preds }
let translate_type_id (id : T.type_id) : type_id =
match id with
@@ -564,7 +547,7 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
| TLiteral lty -> TLiteral lty
| TRef (_, rty, _) -> translate rty
| TRawPtr (ty, rkind) ->
- let mut = match rkind with Mut -> Mut | Shared -> 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)
@@ -655,10 +638,10 @@ let rec translate_back_ty (type_infos : TA.type_infos)
| TLiteral lty -> wrap (TLiteral lty)
| TRef (r, rty, rkind) -> (
match rkind with
- | T.Shared ->
+ | RShared ->
(* Ignore shared references, unless we are below a mutable borrow *)
if inside_mut then translate rty else None
- | T.Mut ->
+ | RMut ->
(* Dive in, remembering the fact that we are inside a mutable borrow *)
let inside_mut = true in
if keep_region r then
@@ -1034,7 +1017,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
effect_info;
}
in
- let preds = translate_predicates sg.A.preds in
+ let preds = translate_predicates sg.preds in
let sg = { generics; preds; inputs; output; doutputs; info } in
{ sg; output_names }
@@ -1795,7 +1778,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
log#ldebug
(lazy
("translate_end_abstraction_synth_input:" ^ "\n- function: "
- ^ Print.name_to_string ctx.fun_decl.name
+ ^ name_to_string ctx ctx.fun_decl.name
^ "\n- rg_id: "
^ T.RegionGroupId.to_string rg_id
^ "\n- loop_id: "
@@ -2109,7 +2092,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
(* Actually the same case as [SynthInput] *)
translate_end_abstraction_synth_input ectx abs e ctx rg_id
| V.LoopCall ->
- let fun_id = E.FRegular ctx.fun_decl.A.def_id in
+ let fun_id = E.FRegular ctx.fun_decl.def_id in
let effect_info =
get_fun_effect_info ctx.fun_context.fun_infos (FunId fun_id)
(Some vloop_id) (Some rg_id)
@@ -2336,7 +2319,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
(* We don't need to update the context: we don't introduce any
* new values/variables *)
let branch = translate_expression branch_e ctx in
- let pat = mk_typed_pattern_from_literal (PV.VScalar v) in
+ let pat = mk_typed_pattern_from_literal (VScalar v) in
{ pat; branch }
in
let branches = List.map translate_branch branches in
@@ -2569,7 +2552,7 @@ and translate_forward_end (ectx : C.eval_ctx)
let org_args = args in
(* Lookup the effect info for the loop function *)
- let fid = E.FRegular ctx.fun_decl.A.def_id in
+ let fid = E.FRegular ctx.fun_decl.def_id in
let effect_info =
get_fun_effect_info ctx.fun_context.fun_infos (FunId fid) None ctx.bid
in
@@ -2918,14 +2901,15 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
log#ldebug
(lazy
("SymbolicToPure.translate_fun_decl: "
- ^ Print.fun_name_to_string def.A.name
+ ^ name_to_string ctx def.name
^ " ("
^ Print.option_to_string T.RegionGroupId.to_string bid
^ ")\n"));
(* Translate the declaration *)
- let def_id = def.A.def_id in
- let basename = def.name in
+ let def_id = def.def_id in
+ let llbc_name = def.name in
+ let name = name_to_string ctx llbc_name in
(* Retrieve the signature *)
let signature = ctx.sg in
let regions_hierarchy =
@@ -2999,7 +2983,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
log#ldebug
(lazy
("SymbolicToPure.translate_fun_decl: "
- ^ Print.fun_name_to_string def.A.name
+ ^ name_to_string ctx def.name
^ " ("
^ Print.option_to_string T.RegionGroupId.to_string bid
^ ")" ^ "\n- forward_inputs: "
@@ -3030,14 +3014,15 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
let loop_id = None in
(* Assemble the declaration *)
- let def =
+ let def : fun_decl =
{
def_id;
kind = def.kind;
num_loops;
loop_id;
back_id = bid;
- basename;
+ llbc_name;
+ name;
signature;
is_global_decl_body = def.is_global_decl_body;
body;
@@ -3051,8 +3036,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
(* return *)
def
-let translate_type_decls (type_decls : T.type_decl list) : type_decl list =
- List.map translate_type_decl type_decls
+let translate_type_decls (ctx : Contexts.decls_ctx)
+ (type_decls : T.type_decl list) : type_decl list =
+ List.map (translate_type_decl ctx) type_decls
(** Translates function signatures.
@@ -3105,11 +3091,11 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx)
(fun m (id, sg) -> RegularFunIdNotLoopMap.add id sg m)
RegularFunIdNotLoopMap.empty translated
-let translate_trait_decl (type_infos : TA.type_infos)
- (trait_decl : A.trait_decl) : trait_decl =
+let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
+ : trait_decl =
let {
def_id;
- name;
+ name = llbc_name;
generics;
preds;
parent_clauses;
@@ -3120,6 +3106,12 @@ let translate_trait_decl (type_infos : TA.type_infos)
} : A.trait_decl =
trait_decl
in
+ let type_infos = ctx.type_ctx.type_infos in
+ let name =
+ Print.Types.name_to_string
+ (Print.Contexts.decls_ctx_to_fmt_env ctx)
+ llbc_name
+ in
let generics = translate_generic_params generics in
let preds = translate_predicates preds in
let parent_clauses = List.map translate_trait_clause parent_clauses in
@@ -3138,6 +3130,7 @@ let translate_trait_decl (type_infos : TA.type_infos)
in
{
def_id;
+ llbc_name;
name;
generics;
preds;
@@ -3148,11 +3141,11 @@ let translate_trait_decl (type_infos : TA.type_infos)
provided_methods;
}
-let translate_trait_impl (type_infos : TA.type_infos)
- (trait_impl : A.trait_impl) : trait_impl =
+let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
+ : trait_impl =
let {
A.def_id;
- name;
+ name = llbc_name;
impl_trait;
generics;
preds;
@@ -3164,9 +3157,15 @@ let translate_trait_impl (type_infos : TA.type_infos)
} =
trait_impl
in
+ let type_infos = ctx.type_ctx.type_infos in
let impl_trait =
translate_trait_decl_ref (translate_fwd_ty type_infos) impl_trait
in
+ let name =
+ Print.Types.name_to_string
+ (Print.Contexts.decls_ctx_to_fmt_env ctx)
+ llbc_name
+ in
let generics = translate_generic_params generics in
let preds = translate_predicates preds in
let parent_trait_refs = List.map translate_strait_ref parent_trait_refs in
@@ -3185,6 +3184,7 @@ let translate_trait_impl (type_infos : TA.type_infos)
in
{
def_id;
+ llbc_name;
name;
impl_trait;
generics;
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-21 16:42:01 +0000