summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Contexts.ml11
-rw-r--r--src/ExtractToFStar.ml11
-rw-r--r--src/FunsAnalysis.ml6
-rw-r--r--src/Interpreter.ml44
-rw-r--r--src/InterpreterStatements.ml3
-rw-r--r--src/LlbcAst.ml21
-rw-r--r--src/LlbcOfJson.ml73
-rw-r--r--src/Modules.ml11
-rw-r--r--src/Names.ml2
-rw-r--r--src/Print.ml23
-rw-r--r--src/PrintPure.ml9
-rw-r--r--src/Pure.ml2
-rw-r--r--src/PureToExtract.ml7
-rw-r--r--src/SymbolicToPure.ml23
-rw-r--r--src/Translate.ml21
-rw-r--r--src/TranslateCore.ml17
16 files changed, 172 insertions, 112 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 1fbc916b..4f1e1506 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -219,13 +219,18 @@ type type_context = {
type fun_context = {
fun_decls : fun_decl FunDeclId.Map.t;
- gid_conv : global_id_converter;
+}
+[@@deriving show]
+
+type global_context = {
+ global_decls : global_decl GlobalDeclId.Map.t;
}
[@@deriving show]
type eval_ctx = {
type_context : type_context;
fun_context : fun_context;
+ global_context : global_context;
type_vars : type_var list;
env : env;
ended_regions : RegionId.Set.t;
@@ -260,8 +265,8 @@ let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl =
FunDeclId.Map.find fid ctx.fun_context.fun_decls
(** TODO: make this more efficient with maps *)
-let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : fun_decl =
- ctx_lookup_fun_decl ctx (global_to_fun_id ctx.fun_context.gid_conv gid)
+let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : global_decl =
+ GlobalDeclId.Map.find gid ctx.global_context.global_decls
(** Retrieve a variable's value in an environment *)
let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 5b39b0b7..2c53e45b 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -907,9 +907,12 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
| Func fun_id ->
extract_function_call ctx fmt inside fun_id qualif.type_args args
| Global global_id ->
+ failwith "TODO ExtractToFStar.ml:911"
+ (* Previous code:
let fid = A.global_to_fun_id ctx.trans_ctx.fun_context.gid_conv global_id in
let fun_id = Regular (A.Regular fid, None) in
extract_function_call ctx fmt inside fun_id qualif.type_args args
+ *)
| AdtCons adt_cons_id ->
extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args
| Proj proj ->
@@ -1485,7 +1488,7 @@ let global_decl_to_body_name (decl : string) : string =
assert (String.sub decl base_len 2 = "_c");
(String.sub decl 0 base_len) ^ "_body"
-(** Print a definition of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *)
+(** Extract a global definition of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *)
let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter)
(qualif : fun_decl_qualif) (name : string) (ty : ty)
(extract_body : (F.formatter -> unit) Option.t)
@@ -1550,8 +1553,11 @@ let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter)
let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
(qualif : fun_decl_qualif) (def : fun_decl)
: unit =
+ (* TODO Lookup LLBC decl *)
(* Sanity checks for globals *)
- assert (def.is_global);
+ assert (def.is_global_body);
+ failwith "TODO ExtractToFStar.ml:1559"
+ (* Previous code:
assert (Option.is_none def.back_id);
assert (List.length def.signature.inputs = 0);
assert (List.length def.signature.doutputs = 1);
@@ -1578,6 +1584,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt ("eval_global " ^ body_name)
));
F.pp_print_break fmt 0 0
+ *)
(** Extract a unit test, if the function is a unit function (takes no
parameters, returns unit).
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index b1b8ccc2..034575c0 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -61,7 +61,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
* (we check that it is successful in the extracted code: if it is
* not, it leads to a type-checking error in the generated files)
*)
- if f.is_global then () else
+ if f.is_global_body then () else
can_fail := !can_fail || b
method! visit_Assert env a =
@@ -98,7 +98,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
super#visit_Loop env loop
end
in
- assert (not f.is_global || not use_state);
+ assert (not f.is_global_body || not use_state);
(match f.body with
| None ->
(* Opaque function *)
@@ -108,7 +108,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
(* We ignore on purpose functions that cannot fail: the result of the analysis
* is not used yet to adjust the translation so that the functions which
* syntactically can't fail don't use an error monad. *)
- can_fail := not f.is_global
+ can_fail := not f.is_global_body
in
List.iter visit_fun d;
{ can_fail = !can_fail; stateful = !stateful; divergent = !divergent }
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index f4f01ff8..3610d486 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -14,9 +14,9 @@ module SA = SymbolicAst
let log = L.interpreter_log
let compute_type_fun_contexts (m : M.llbc_module) :
- C.type_context * C.fun_context =
+ C.type_context * C.fun_context * C.global_context =
let type_decls_list, _ = M.split_declarations m.declarations in
- let type_decls, fun_decls = M.compute_defs_maps m in
+ let type_decls, fun_decls, global_decls = M.compute_defs_maps m in
let type_decls_groups, _funs_defs_groups =
M.split_declarations_to_group_maps m.declarations
in
@@ -24,15 +24,20 @@ let compute_type_fun_contexts (m : M.llbc_module) :
TypesAnalysis.analyze_type_declarations type_decls type_decls_list
in
let type_context = { C.type_decls_groups; type_decls; type_infos } in
- let fun_context = { C.fun_decls; gid_conv = m.gid_conv } in
- (type_context, fun_context)
-
-let initialize_eval_context (type_context : C.type_context)
- (fun_context : C.fun_context) (type_vars : T.type_var list) : C.eval_ctx =
+ let fun_context = { C.fun_decls } in
+ let global_context = { C.global_decls } in
+ (type_context, fun_context, global_context)
+
+let initialize_eval_context
+ (type_context : C.type_context)
+ (fun_context : C.fun_context)
+ (global_context : C.global_context)
+ (type_vars : T.type_var list) : C.eval_ctx =
C.reset_global_counters ();
{
C.type_context;
C.fun_context;
+ C.global_context;
C.type_vars;
C.env = [ C.Frame ];
C.ended_regions = T.RegionId.Set.empty;
@@ -51,8 +56,11 @@ let initialize_eval_context (type_context : C.type_context)
- the list of symbolic values introduced for the input values
- the instantiated function signature
*)
-let initialize_symbolic_context_for_fun (type_context : C.type_context)
- (fun_context : C.fun_context) (fdef : A.fun_decl) :
+let initialize_symbolic_context_for_fun
+ (type_context : C.type_context)
+ (fun_context : C.fun_context)
+ (global_context : C.global_context)
+ (fdef : A.fun_decl) :
C.eval_ctx * V.symbolic_value list * A.inst_fun_sig =
(* The abstractions are not initialized the same way as for function
* calls: they contain *loan* projectors, because they "provide" us
@@ -67,7 +75,7 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context)
* *)
let sg = fdef.signature in
(* Create the context *)
- let ctx = initialize_eval_context type_context fun_context sg.type_params in
+ let ctx = initialize_eval_context type_context fun_context global_context sg.type_params in
(* Instantiate the signature *)
let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in
let inst_sg = instantiate_fun_sig type_params sg in
@@ -204,7 +212,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
- the symbolic AST generated by the symbolic execution
*)
let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
- (type_context : C.type_context) (fun_context : C.fun_context)
+ (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context)
(fdef : A.fun_decl) (back_id : T.RegionGroupId.id option) :
V.symbolic_value list * SA.expression option =
(* Debug *)
@@ -218,7 +226,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
(* Create the evaluation context *)
let ctx, input_svs, inst_sg =
- initialize_symbolic_context_for_fun type_context fun_context fdef
+ initialize_symbolic_context_for_fun type_context fun_context global_context fdef
in
(* Create the continuation to finish the evaluation *)
@@ -285,8 +293,8 @@ module Test = struct
assert (body.A.arg_count = 0);
(* Create the evaluation context *)
- let type_context, fun_context = compute_type_fun_contexts m in
- let ctx = initialize_eval_context type_context fun_context [] in
+ let type_context, fun_context, global_context = compute_type_fun_contexts m in
+ let ctx = initialize_eval_context type_context fun_context global_context [] in
(* Insert the (uninitialized) local variables *)
let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in
@@ -330,7 +338,7 @@ module Test = struct
(** Execute the symbolic interpreter on a function. *)
let test_function_symbolic (config : C.partial_config) (synthesize : bool)
- (type_context : C.type_context) (fun_context : C.fun_context)
+ (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context)
(fdef : A.fun_decl) : unit =
(* Debug *)
log#ldebug
@@ -338,7 +346,7 @@ module Test = struct
(* Evaluate *)
let evaluate =
- evaluate_function_symbolic config synthesize type_context fun_context fdef
+ evaluate_function_symbolic config synthesize type_context fun_context global_context fdef
in
(* Execute the forward function *)
let _ = evaluate None in
@@ -368,12 +376,12 @@ module Test = struct
in
(* Filter the opaque functions *)
let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in
- let type_context, fun_context = compute_type_fun_contexts m in
+ let type_context, fun_context, global_context = compute_type_fun_contexts m in
let test_fun (def : A.fun_decl) : unit =
(* Execute the function - note that as the symbolic interpreter explores
* all the path, some executions are expected to "panic": we thus don't
* check the return value *)
- test_function_symbolic config synthesize type_context fun_context def
+ test_function_symbolic config synthesize type_context fun_context global_context def
in
List.iter test_fun no_loop_funs
end
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 8f981174..6a0b81f3 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -832,8 +832,9 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
(* Compose and apply *)
comp cf_eval_rvalue cf_assign cf ctx
| A.AssignGlobal { dst; global } ->
+ (* What codegen do we want ? *)
let call : A.call = {
- func = A.Regular (A.global_to_fun_id ctx.fun_context.gid_conv global);
+ func = A.Regular (failwith "TODO InterpretStatements.ml:837");
region_args = [];
type_args = [];
args = [];
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index 16733e20..aa9b0665 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -7,17 +7,6 @@ open Identifiers
module FunDeclId = IdGen ()
module GlobalDeclId = IdGen ()
-(* Strict type for the number of function declarations (see [global_to_fun_id] below) *)
-type global_id_converter = { fun_count : int }
-[@@deriving show]
-
-(** Converts a global id to its corresponding function id.
- To do so, it adds the global id to the number of function declarations :
- We have the bijection `global_id <=> fun_id + fun_id_count`.
-*)
-let global_to_fun_id (conv : global_id_converter) (gid : GlobalDeclId.id) : FunDeclId.id =
- FunDeclId.of_int ((GlobalDeclId.to_int gid) + conv.fun_count)
-
type var = {
index : VarId.id; (** Unique variable identifier *)
name : string option;
@@ -201,6 +190,14 @@ type fun_decl = {
name : fun_name;
signature : fun_sig;
body : fun_body option;
- is_global : bool;
+ is_global_body : bool;
+}
+[@@deriving show]
+
+type global_decl = {
+ def_id : GlobalDeclId.id;
+ body_id: FunDeclId.id;
+ name : global_name;
+ ty: ety;
}
[@@deriving show]
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index c157b667..f51c15be 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -540,7 +540,7 @@ let call_of_json (js : json) : (A.call, string) result =
Ok { A.func; region_args; type_args; args; dest }
| _ -> Error "")
-let rec statement_of_json (js : json) (gid_conv : A.global_id_converter) : (A.statement, string) result =
+let rec statement_of_json (js : json) : (A.statement, string) result =
combine_error_msgs js "statement_of_json"
(match js with
| `Assoc [ ("Assign", `List [ place; rvalue ]) ] ->
@@ -577,48 +577,49 @@ let rec statement_of_json (js : json) (gid_conv : A.global_id_converter) : (A.st
Ok (A.Continue i)
| `String "Nop" -> Ok A.Nop
| `Assoc [ ("Sequence", `List [ st1; st2 ]) ] ->
- let* st1 = statement_of_json st1 gid_conv in
- let* st2 = statement_of_json st2 gid_conv in
+ let* st1 = statement_of_json st1 in
+ let* st2 = statement_of_json st2 in
Ok (A.Sequence (st1, st2))
| `Assoc [ ("Switch", `List [ op; tgt ]) ] ->
let* op = operand_of_json op in
- let* tgt = switch_targets_of_json tgt gid_conv in
+ let* tgt = switch_targets_of_json tgt in
Ok (A.Switch (op, tgt))
| `Assoc [ ("Loop", st) ] ->
- let* st = statement_of_json st gid_conv in
+ let* st = statement_of_json st in
Ok (A.Loop st)
| _ -> Error "")
-and switch_targets_of_json (js : json) (gid_conv : A.global_id_converter) : (A.switch_targets, string) result =
+and switch_targets_of_json (js : json) : (A.switch_targets, string) result =
combine_error_msgs js "switch_targets_of_json"
(match js with
| `Assoc [ ("If", `List [ st1; st2 ]) ] ->
- let* st1 = statement_of_json st1 gid_conv in
- let* st2 = statement_of_json st2 gid_conv in
+ let* st1 = statement_of_json st1 in
+ let* st2 = statement_of_json st2 in
Ok (A.If (st1, st2))
| `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] ->
let* int_ty = integer_type_of_json int_ty in
let* tgts =
- list_of_json (pair_of_json
+ list_of_json (
+ pair_of_json
(list_of_json scalar_value_of_json)
- (fun js -> statement_of_json js gid_conv))
+ statement_of_json)
tgts
in
- let* otherwise = statement_of_json otherwise gid_conv in
+ let* otherwise = statement_of_json otherwise in
Ok (A.SwitchInt (int_ty, tgts, otherwise))
| _ -> Error "")
-let fun_body_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_body, string) result =
+let fun_body_of_json (js : json) : (A.fun_body, string) result =
combine_error_msgs js "fun_body_of_json"
(match js with
| `Assoc [ ("arg_count", arg_count); ("locals", locals); ("body", body) ] ->
let* arg_count = int_of_json arg_count in
let* locals = list_of_json var_of_json locals in
- let* body = statement_of_json body gid_conv in
+ let* body = statement_of_json body in
Ok { A.arg_count; locals; body }
| _ -> Error "")
-let fun_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result =
+let fun_decl_of_json (js : json) : (A.fun_decl, string) result =
combine_error_msgs js "fun_decl_of_json"
(match js with
| `Assoc
@@ -631,13 +632,24 @@ let fun_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_dec
let* def_id = A.FunDeclId.id_of_json def_id in
let* name = fun_name_of_json name in
let* signature = fun_sig_of_json signature in
- let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in
- Ok { A.def_id; name; signature; body; is_global = false; }
+ let* body = option_of_json fun_body_of_json body in
+ Ok { A.def_id; name; signature; body; is_global_body = false; }
| _ -> Error "")
+(* Strict type for the number of function declarations (see [global_to_fun_id] below) *)
+type global_id_converter = { fun_count : int }
+[@@deriving show]
+
+(** Converts a global id to its corresponding function id.
+ To do so, it adds the global id to the number of function declarations :
+ We have the bijection `global_id <=> fun_id + fun_id_count`.
+*)
+let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) : A.FunDeclId.id =
+ A.FunDeclId.of_int ((A.GlobalDeclId.to_int gid) + conv.fun_count)
+
(* Converts a global declaration to a function declaration.
*)
-let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result =
+let global_decl_of_json (js : json) (gid_conv : global_id_converter) : (A.global_decl * A.fun_decl, string) result =
combine_error_msgs js "global_decl_of_json"
(match js with
| `Assoc
@@ -648,10 +660,10 @@ let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_
("body", body);
] ->
let* global_id = A.GlobalDeclId.id_of_json def_id in
- let def_id = A.global_to_fun_id gid_conv global_id in
+ let fun_id = global_to_fun_id gid_conv global_id in
let* name = fun_name_of_json name in
let* ty = ety_of_json ty in
- let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in
+ let* body = option_of_json fun_body_of_json body in
let signature : A.fun_sig = {
region_params = [];
num_early_bound_regions = 0;
@@ -660,7 +672,8 @@ let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_
inputs = [];
output = TU.ety_no_regions_to_sty ty;
} in
- Ok { A.def_id; name; signature; body; is_global = true; }
+ Ok ({ A.def_id = global_id; body_id = fun_id; name; ty; },
+ { A.def_id = fun_id; name; signature; body; is_global_body = true; })
| _ -> Error "")
let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
@@ -685,15 +698,18 @@ let fun_declaration_group_of_json (js : json) :
combine_error_msgs js "fun_declaration_group_of_json"
(g_declaration_group_of_json A.FunDeclId.id_of_json js)
-let global_declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) :
+(* TODO Should a global declaration group be converted to its function bodies ?
+ It does not seems very clean.
+*)
+let global_declaration_group_of_json (js : json) (gid_conv : global_id_converter) :
(M.fun_declaration_group, string) result =
combine_error_msgs js "global_declaration_group_of_json"
(g_declaration_group_of_json (fun js ->
let* id = A.GlobalDeclId.id_of_json js in
- Ok (A.global_to_fun_id gid_conv id)
+ Ok (global_to_fun_id gid_conv id)
) js)
-let declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) : (M.declaration_group, string) result
+let declaration_group_of_json (js : json) (gid_conv : global_id_converter) : (M.declaration_group, string) result
=
combine_error_msgs js "declaration_of_json"
(match js with
@@ -726,19 +742,20 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
("globals", globals);
] ->
let* fun_count = length_of_json_list functions in
- let gid_conv = { A.fun_count = fun_count } in
+ let gid_conv = { fun_count } in
let* name = string_of_json name in
let* declarations =
list_of_json (fun js -> declaration_group_of_json js gid_conv) declarations
in
- let* types = list_of_json type_decl_of_json types in
- let* functions = list_of_json (fun js -> fun_decl_of_json js gid_conv) functions in
+ let* types = list_of_json type_decl_of_json types in
+ let* functions = list_of_json fun_decl_of_json functions in
let* globals = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in
+ let globals, global_bodies = List.split globals in
Ok {
M.name;
declarations;
types;
- functions = functions @ globals;
- gid_conv;
+ functions = functions @ global_bodies;
+ globals;
}
| _ -> Error "")
diff --git a/src/Modules.ml b/src/Modules.ml
index 149de020..2f640636 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -21,12 +21,12 @@ type llbc_module = {
declarations : declaration_group list;
types : type_decl list;
functions : fun_decl list;
- gid_conv : global_id_converter;
+ globals : global_decl list;
}
(** LLBC module - TODO: rename to crate *)
let compute_defs_maps (m : llbc_module) :
- type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t =
+ type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t * global_decl GlobalDeclId.Map.t =
let types_map =
List.fold_left
(fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m)
@@ -37,7 +37,12 @@ let compute_defs_maps (m : llbc_module) :
(fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m)
FunDeclId.Map.empty m.functions
in
- (types_map, funs_map)
+ let globals_map =
+ List.fold_left
+ (fun m (def : global_decl) -> GlobalDeclId.Map.add def.def_id def m)
+ GlobalDeclId.Map.empty m.globals
+ in
+ (types_map, funs_map, globals_map)
(** Split a module's declarations between types and functions *)
let split_declarations (decls : declaration_group list) :
diff --git a/src/Names.ml b/src/Names.ml
index 1308eccc..0db5291a 100644
--- a/src/Names.ml
+++ b/src/Names.ml
@@ -54,6 +54,8 @@ type type_name = name [@@deriving show, ord]
type fun_name = name [@@deriving show, ord]
+type global_name = name [@@deriving show, ord]
+
(** Filter the disambiguators equal to 0 in a name *)
let filter_disambiguators_zero (n : name) : name =
let pred (pe : path_elem) : bool =
diff --git a/src/Print.ml b/src/Print.ml
index 337116ec..6b11a3ff 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -13,6 +13,7 @@ let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
let name_to_string (name : name) : string = Names.name_to_string name
let fun_name_to_string (name : fun_name) : string = name_to_string name
+let global_name_to_string (name : global_name) : string = name_to_string name
(** Pretty-printing for types *)
module Types = struct
@@ -744,7 +745,8 @@ module LlbcAst = struct
fun_name_to_string def.name
in
let global_decl_id_to_string def_id =
- fun_decl_id_to_string (A.global_to_fun_id ctx.fun_context.gid_conv def_id)
+ let def = C.ctx_lookup_global_decl ctx def_id in
+ global_name_to_string def.name
in
{
rvar_to_string = ctx_fmt.PV.rvar_to_string;
@@ -762,7 +764,7 @@ module LlbcAst = struct
let fun_decl_to_ast_formatter
(type_decls : T.type_decl T.TypeDeclId.Map.t)
(fun_decls : A.fun_decl A.FunDeclId.Map.t)
- (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id)
+ (global_decls : A.global_decl A.GlobalDeclId.Map.t)
(fdef : A.fun_decl) :
ast_formatter =
let rvar_to_string r =
@@ -793,7 +795,8 @@ module LlbcAst = struct
fun_name_to_string def.name
in
let global_decl_id_to_string def_id =
- fun_decl_id_to_string (global_to_fun_id def_id)
+ let def = A.GlobalDeclId.Map.find def_id global_decls in
+ global_name_to_string def.name
in
{
rvar_to_string;
@@ -1132,7 +1135,7 @@ module Module = struct
let def_ctx_to_ast_formatter
(type_context : T.type_decl T.TypeDeclId.Map.t)
(fun_context : A.fun_decl A.FunDeclId.Map.t)
- (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id)
+ (global_context : A.global_decl A.GlobalDeclId.Map.t)
(def : A.fun_decl) :
PA.ast_formatter =
let rvar_to_string vid =
@@ -1156,7 +1159,8 @@ module Module = struct
fun_name_to_string def.name
in
let global_decl_id_to_string def_id =
- fun_decl_id_to_string (global_to_fun_id def_id)
+ let def = A.GlobalDeclId.Map.find def_id global_context in
+ global_name_to_string def.name
in
let var_id_to_string vid =
let var = V.VarId.nth (Option.get def.body).locals vid in
@@ -1187,21 +1191,20 @@ module Module = struct
let fun_decl_to_string
(type_context : T.type_decl T.TypeDeclId.Map.t)
(fun_context : A.fun_decl A.FunDeclId.Map.t)
- (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id)
+ (global_context : A.global_decl A.GlobalDeclId.Map.t)
(def : A.fun_decl) : string =
- let fmt = def_ctx_to_ast_formatter type_context fun_context global_to_fun_id def in
+ let fmt = def_ctx_to_ast_formatter type_context fun_context global_context def in
PA.fun_decl_to_string fmt "" " " def
let module_to_string (m : M.llbc_module) : string =
- let types_defs_map, funs_defs_map = M.compute_defs_maps m in
+ let types_defs_map, funs_defs_map, globals_defs_map = M.compute_defs_maps m in
(* The types *)
let type_decls = List.map (type_decl_to_string types_defs_map) m.M.types in
(* The functions *)
let fun_decls =
- let gid_to_fid = fun gid -> A.global_to_fun_id m.gid_conv gid in
- List.map (fun_decl_to_string types_defs_map funs_defs_map gid_to_fid) m.M.functions
+ List.map (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map) m.M.functions
in
(* Put everything together *)
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index c13f967f..597330bf 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -62,6 +62,7 @@ let ast_to_type_formatter (fmt : ast_formatter) : type_formatter =
let name_to_string = Print.name_to_string
let fun_name_to_string = Print.fun_name_to_string
+let global_name_to_string = Print.global_name_to_string
let option_to_string = Print.option_to_string
let type_var_to_string = Print.Types.type_var_to_string
let integer_type_to_string = Print.Types.integer_type_to_string
@@ -85,9 +86,10 @@ let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
functions (there is a difference between the forward/backward functions...)
while we only need those definitions to lookup proper names for the def ids.
*)
-let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
+let mk_ast_formatter
+ (type_decls : T.type_decl TypeDeclId.Map.t)
(fun_decls : A.fun_decl A.FunDeclId.Map.t)
- (gid_conv : A.global_id_converter)
+ (global_decls : A.global_decl A.GlobalDeclId.Map.t)
(type_params : type_var list) :
ast_formatter =
let type_var_id_to_string vid =
@@ -116,7 +118,8 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
fun_name_to_string def.name
in
let global_decl_id_to_string def_id =
- fun_decl_id_to_string (A.global_to_fun_id gid_conv def_id)
+ let def = A.GlobalDeclId.Map.find def_id global_decls in
+ global_name_to_string def.name
in
{
type_var_id_to_string;
diff --git a/src/Pure.ml b/src/Pure.ml
index b3be2040..5244b0bc 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -575,6 +575,6 @@ type fun_decl = {
(to identify the forward/backward functions) later.
*)
signature : fun_sig;
- is_global : bool;
+ is_global_body : bool;
body : fun_body option;
}
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index e58fec2a..7a10bb6b 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -83,14 +83,15 @@ type formatter = {
- function id: this is especially useful to identify whether the
function is an assumed function or a local function
- function basename
+ - flag indicating if the function is a global
- number of region groups
+ - region group information in case of a backward function
+ (`None` if forward function)
- pair:
- do we generate the forward function (it may have been filtered)?
- the number of extracted backward functions (not necessarily equal
to the number of region groups, because we may have filtered
some of them)
- - region group information in case of a backward function
- (`None` if forward function)
TODO: use the fun id for the assumed functions.
*)
decreases_clause_name : A.FunDeclId.id -> fun_name -> string;
@@ -599,7 +600,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
in
let def_id = A.Regular def_id in
let name =
- ctx.fmt.fun_name def_id def.basename def.is_global num_rgs rg_info (keep_fwd, num_backs)
+ ctx.fmt.fun_name def_id def.basename def.is_global_body num_rgs rg_info (keep_fwd, num_backs)
in
(* Add the function name *)
let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index a057b015..7d9e2906 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -70,7 +70,10 @@ type fun_context = {
llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
fun_sigs : fun_sig_named_outputs RegularFunIdMap.t; (** *)
fun_infos : FA.fun_info A.FunDeclId.Map.t;
- gid_conv : A.global_id_converter;
+}
+
+type global_context = {
+ llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t;
}
type call_info = {
@@ -96,6 +99,7 @@ type call_info = {
type bs_ctx = {
type_context : type_context;
fun_context : fun_context;
+ global_context : global_context;
fun_decl : A.fun_decl;
bid : T.RegionGroupId.id option; (** TODO: rename *)
sg : fun_sig;
@@ -137,15 +141,15 @@ let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.LlbcAst.ast_formatter =
Print.LlbcAst.fun_decl_to_ast_formatter
ctx.type_context.llbc_type_decls
ctx.fun_context.llbc_fun_decls
- (A.global_to_fun_id ctx.fun_context.gid_conv)
+ ctx.global_context.llbc_global_decls
ctx.fun_decl
let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
let type_params = ctx.fun_decl.signature.type_params in
let type_decls = ctx.type_context.llbc_type_decls in
let fun_decls = ctx.fun_context.llbc_fun_decls in
- let gid_conv = ctx.fun_context.gid_conv in
- PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params
+ let global_decls = ctx.global_context.llbc_global_decls in
+ PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
let ty_to_string (ctx : bs_ctx) (ty : ty) : string =
let fmt = bs_ctx_to_pp_ast_formatter ctx in
@@ -166,16 +170,16 @@ let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
let type_params = sg.type_params in
let type_decls = ctx.type_context.llbc_type_decls in
let fun_decls = ctx.fun_context.llbc_fun_decls in
- let gid_conv = ctx.fun_context.gid_conv in
- let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in
+ let global_decls = ctx.global_context.llbc_global_decls in
+ let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in
PrintPure.fun_sig_to_string fmt sg
let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
let type_params = def.signature.type_params in
let type_decls = ctx.type_context.llbc_type_decls in
let fun_decls = ctx.fun_context.llbc_fun_decls in
- let gid_conv = ctx.fun_context.gid_conv in
- let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in
+ let global_decls = ctx.global_context.llbc_global_decls in
+ let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in
PrintPure.fun_decl_to_string fmt def
(* TODO: move *)
@@ -1666,7 +1670,6 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
(* Lookup the signature *)
let signature = bs_ctx_lookup_local_function_sig def_id bid ctx in
(* Translate the body, if there is *)
- let is_global = def.A.is_global in
let body =
match body with
| None -> None
@@ -1727,7 +1730,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
Some { inputs; inputs_lvs; body }
in
(* Assemble the declaration *)
- let def = { def_id; back_id = bid; basename; signature; is_global; body } in
+ let def = { def_id; back_id = bid; basename; signature; is_global_body = def.is_global_body; body } in
(* Debugging *)
log#ldebug
(lazy
diff --git a/src/Translate.ml b/src/Translate.ml
index 9412b8b8..a6477e7f 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -63,10 +63,9 @@ let translate_function_to_symbolics (config : C.partial_config)
("translate_function_to_symbolics: "
^ Print.fun_name_to_string fdef.A.name));
- let { type_context; fun_context } = trans_ctx in
+ let { type_context; fun_context; global_context } = trans_ctx in
let fun_context = {
C.fun_decls = fun_context.fun_decls;
- C.gid_conv = fun_context.gid_conv;
} in
match fdef.body with
@@ -76,7 +75,8 @@ let translate_function_to_symbolics (config : C.partial_config)
let synthesize = true in
let evaluate gid =
let inputs, symb =
- evaluate_function_symbolic config synthesize type_context fun_context
+ evaluate_function_symbolic config synthesize
+ type_context fun_context global_context
fdef gid
in
(inputs, Option.get symb)
@@ -110,7 +110,7 @@ let translate_function_to_pure (config : C.partial_config)
(lazy
("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name));
- let { type_context; fun_context } = trans_ctx in
+ let { type_context; fun_context; global_context } = trans_ctx in
let def_id = fdef.def_id in
(* Compute the symbolic ASTs, if the function is transparent *)
@@ -142,7 +142,10 @@ let translate_function_to_pure (config : C.partial_config)
SymbolicToPure.llbc_fun_decls = fun_context.fun_decls;
fun_sigs;
fun_infos = fun_context.fun_infos;
- gid_conv = fun_context.gid_conv;
+ }
+ in
+ let global_context = {
+ SymbolicToPure.llbc_global_decls = global_context.global_decls
}
in
let ctx =
@@ -156,6 +159,7 @@ let translate_function_to_pure (config : C.partial_config)
state_var;
type_context;
fun_context;
+ global_context;
fun_decl = fdef;
forward_inputs = [];
(* Empty for now *)
@@ -293,14 +297,13 @@ let translate_module_to_pure (config : C.partial_config)
log#ldebug (lazy "translate_module_to_pure");
(* Compute the type and function contexts *)
- let type_context, fun_context = compute_type_fun_contexts m in
+ let type_context, fun_context, global_context = compute_type_fun_contexts m in
let fun_infos = FA.analyze_module m fun_context.C.fun_decls use_state in
let fun_context = {
fun_decls = fun_context.fun_decls;
fun_infos;
- gid_conv = m.gid_conv;
} in
- let trans_ctx = { type_context; fun_context } in
+ let trans_ctx = { type_context; fun_context; global_context } in
(* Translate all the type definitions *)
let type_decls = SymbolicToPure.translate_type_decls m.types in
@@ -495,7 +498,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
if
((not is_opaque) && config.extract_transparent)
|| (is_opaque && config.extract_opaque)
- then if def.is_global
+ then if def.is_global_body
then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt qualif def
else ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def
)
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index 047219ad..e77445cd 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -16,11 +16,16 @@ type type_context = C.type_context [@@deriving show]
type fun_context = {
fun_decls : A.fun_decl A.FunDeclId.Map.t;
fun_infos : FA.fun_info A.FunDeclId.Map.t;
- gid_conv : A.global_id_converter;
}
[@@deriving show]
-type trans_ctx = { type_context : type_context; fun_context : fun_context }
+type global_context = C.global_context [@@deriving show]
+
+type trans_ctx = {
+ type_context : type_context;
+ fun_context : fun_context;
+ global_context : global_context
+}
type pure_fun_translation = Pure.fun_decl * Pure.fun_decl list
@@ -40,16 +45,16 @@ let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
let type_params = sg.type_params in
let type_decls = ctx.type_context.type_decls in
let fun_decls = ctx.fun_context.fun_decls in
- let gid_conv = ctx.fun_context.gid_conv in
- let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in
+ let global_decls = ctx.global_context.global_decls in
+ let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in
PrintPure.fun_sig_to_string fmt sg
let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
let type_params = def.signature.type_params in
let type_decls = ctx.type_context.type_decls in
let fun_decls = ctx.fun_context.fun_decls in
- let gid_conv = ctx.fun_context.gid_conv in
- let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in
+ let global_decls = ctx.global_context.global_decls in
+ let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in
PrintPure.fun_decl_to_string fmt def
let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string =
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 16:28:15 +0000