summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Contexts.ml1
-rw-r--r--src/Expressions.ml2
-rw-r--r--src/ExtractToFStar.ml1
-rw-r--r--src/FunIdentifier.ml2
-rw-r--r--src/FunsAnalysis.ml1
-rw-r--r--src/Interpreter.ml5
-rw-r--r--src/InterpreterStatements.ml7
-rw-r--r--src/LlbcAst.ml5
-rw-r--r--src/LlbcAstUtils.ml1
-rw-r--r--src/LlbcOfJson.ml146
-rw-r--r--src/Modules.ml1
-rw-r--r--src/Print.ml13
-rw-r--r--src/PrintPure.ml6
-rw-r--r--src/PrintSymbolicAst.ml3
-rw-r--r--src/Pure.ml2
-rw-r--r--src/PureToExtract.ml1
-rw-r--r--src/SymbolicToPure.ml1
-rw-r--r--src/Translate.ml21
-rw-r--r--src/TranslateCore.ml9
-rw-r--r--src/TypesUtils.ml13
20 files changed, 161 insertions, 80 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml
index a4551420..bbf5b8f3 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -1,6 +1,7 @@
open Types
open Values
open LlbcAst
+open FunIdentifier
module V = Values
open ValuesUtils
module M = Modules
diff --git a/src/Expressions.ml b/src/Expressions.ml
index 6bf14c66..f1a4a8c3 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -1,5 +1,6 @@
open Types
open Values
+open FunIdentifier
type field_proj_kind =
| ProjAdt of TypeDeclId.id * VariantId.id option
@@ -88,6 +89,7 @@ let all_binops =
*)
type operand_constant_value =
| ConstantValue of constant_value
+ | ConstantId of FunDeclId.id
| ConstantAdt of VariantId.id option * operand_constant_value list
[@@deriving show]
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 0bbe591e..9766ddaf 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -6,6 +6,7 @@ open PureUtils
open TranslateCore
open PureToExtract
open StringUtils
+open FunIdentifier
module F = Format
(** A qualifier for a type definition.
diff --git a/src/FunIdentifier.ml b/src/FunIdentifier.ml
new file mode 100644
index 00000000..dd7e9318
--- /dev/null
+++ b/src/FunIdentifier.ml
@@ -0,0 +1,2 @@
+open Identifiers
+module FunDeclId = IdGen ()
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index dc205eb9..cf2e0bd6 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -9,6 +9,7 @@
open LlbcAst
open Modules
+open FunIdentifier
type fun_info = {
can_fail : bool;
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index f6ae268d..702aeea6 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1,4 +1,5 @@
open Cps
+open FunIdentifier
open InterpreterUtils
open InterpreterProjectors
open InterpreterBorrows
@@ -255,9 +256,9 @@ module Test = struct
environment.
*)
let test_unit_function (config : C.partial_config) (m : M.llbc_module)
- (fid : A.FunDeclId.id) : unit =
+ (fid : FunDeclId.id) : unit =
(* Retrieve the function declaration *)
- let fdef = A.FunDeclId.nth m.functions fid in
+ let fdef = FunDeclId.nth m.functions fid in
let body = Option.get fdef.body in
(* Debug *)
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 1083d643..c7308720 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -7,6 +7,7 @@ module A = LlbcAst
module L = Logging
open TypesUtils
open ValuesUtils
+open FunIdentifier
module Inv = Invariants
module S = SynthesizeSymbolic
open Errors
@@ -1001,7 +1002,7 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
call.args call.dest
(** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
-and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
+and eval_local_function_call_concrete (config : C.config) (fid : FunDeclId.id)
(region_args : T.erased_region list) (type_args : T.ety list)
(args : E.operand list) (dest : E.place) : st_cm_fun =
fun cf ctx ->
@@ -1079,7 +1080,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
cc cf ctx
(** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
-and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
+and eval_local_function_call_symbolic (config : C.config) (fid : FunDeclId.id)
(region_args : T.erased_region list) (type_args : T.ety list)
(args : E.operand list) (dest : E.place) : st_cm_fun =
fun cf ctx ->
@@ -1300,7 +1301,7 @@ and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id)
(** Evaluate a local (i.e, not assumed) function call (auxiliary helper for
[eval_statement]) *)
-and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id)
+and eval_local_function_call (config : C.config) (fid : FunDeclId.id)
(region_args : T.erased_region list) (type_args : T.ety list)
(args : E.operand list) (dest : E.place) : st_cm_fun =
match config.mode with
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index d35cd5d8..4324586d 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -1,10 +1,8 @@
-open Identifiers
open Names
open Types
open Values
open Expressions
-
-module FunDeclId = IdGen ()
+open FunIdentifier
type var = {
index : VarId.id; (** Unique variable identifier *)
@@ -178,5 +176,6 @@ type fun_decl = {
name : fun_name;
signature : fun_sig;
body : fun_body option;
+ is_global : bool;
}
[@@deriving show]
diff --git a/src/LlbcAstUtils.ml b/src/LlbcAstUtils.ml
index 84e8e00f..bc4236cf 100644
--- a/src/LlbcAstUtils.ml
+++ b/src/LlbcAstUtils.ml
@@ -1,5 +1,6 @@
open LlbcAst
open Utils
+open FunIdentifier
module T = Types
(** Check if a [statement] contains loops *)
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 99d652ec..14333088 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -11,12 +11,14 @@
open Yojson.Basic
open Names
open OfJsonBasic
+open FunIdentifier
module T = Types
module V = Values
module S = Scalars
module M = Modules
module E = Expressions
module A = LlbcAst
+module TU = TypesUtils
(* The default logger *)
let log = Logging.llbc_of_json_logger
@@ -225,6 +227,14 @@ let type_decl_of_json (js : json) : (T.type_decl, string) result =
}
| _ -> Error "")
+(* Converts a global ID to its corresponding function ID.
+ To do so, it adds the global ID to the number of function declarations.
+*)
+let global_id_of_json (js: json) (fun_count: int) : (FunDeclId.id, string) result =
+ combine_error_msgs js "global_id_of_json"
+ (let* gid = FunDeclId.id_of_json js in
+ Ok (FunDeclId.of_int ((FunDeclId.to_int gid) + fun_count)))
+
let var_of_json (js : json) : (A.var, string) result =
combine_error_msgs js "var_of_json"
(match js with
@@ -393,7 +403,7 @@ let binop_of_json (js : json) : (E.binop, string) result =
| `String "Shr" -> Ok E.Shr
| _ -> Error ("binop_of_json failed on:" ^ show js)
-let rec operand_constant_value_of_json (js : json) :
+let rec operand_constant_value_of_json (js : json) (fun_count : int) :
(E.operand_constant_value, string) result =
combine_error_msgs js "operand_constant_value_of_json"
(match js with
@@ -403,12 +413,15 @@ let rec operand_constant_value_of_json (js : json) :
| `Assoc [ ("ConstantAdt", `List [ variant_id; field_values ]) ] ->
let* variant_id = option_of_json T.VariantId.id_of_json variant_id in
let* field_values =
- list_of_json operand_constant_value_of_json field_values
+ list_of_json (fun js -> operand_constant_value_of_json js fun_count) field_values
in
Ok (E.ConstantAdt (variant_id, field_values))
+ | `Assoc [ ("ConstantIdentifier", `List [gid]) ] ->
+ let* id = global_id_of_json gid fun_count in
+ Ok (E.ConstantId id)
| _ -> Error "")
-let operand_of_json (js : json) : (E.operand, string) result =
+let operand_of_json (js : json) (fun_count : int) : (E.operand, string) result =
combine_error_msgs js "operand_of_json"
(match js with
| `Assoc [ ("Copy", place) ] ->
@@ -417,9 +430,9 @@ let operand_of_json (js : json) : (E.operand, string) result =
| `Assoc [ ("Move", place) ] ->
let* place = place_of_json place in
Ok (E.Move place)
- | `Assoc [ ("Constant", `List [ ty; cv ]) ] ->
+ | `Assoc [ ("Const", `List [ ty; cv ]) ] ->
let* ty = ety_of_json ty in
- let* cv = operand_constant_value_of_json cv in
+ let* cv = operand_constant_value_of_json cv fun_count in
Ok (E.Constant (ty, cv))
| _ -> Error "")
@@ -442,11 +455,11 @@ let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result =
Ok (E.AggregatedAdt (id, opt_variant_id, regions, tys))
| _ -> Error "")
-let rvalue_of_json (js : json) : (E.rvalue, string) result =
+let rvalue_of_json (js : json) (fun_count : int) : (E.rvalue, string) result =
combine_error_msgs js "rvalue_of_json"
(match js with
| `Assoc [ ("Use", op) ] ->
- let* op = operand_of_json op in
+ let* op = operand_of_json op fun_count in
Ok (E.Use op)
| `Assoc [ ("Ref", `List [ place; borrow_kind ]) ] ->
let* place = place_of_json place in
@@ -454,19 +467,19 @@ let rvalue_of_json (js : json) : (E.rvalue, string) result =
Ok (E.Ref (place, borrow_kind))
| `Assoc [ ("UnaryOp", `List [ unop; op ]) ] ->
let* unop = unop_of_json unop in
- let* op = operand_of_json op in
+ let* op = operand_of_json op fun_count in
Ok (E.UnaryOp (unop, op))
| `Assoc [ ("BinaryOp", `List [ binop; op1; op2 ]) ] ->
let* binop = binop_of_json binop in
- let* op1 = operand_of_json op1 in
- let* op2 = operand_of_json op2 in
+ let* op1 = operand_of_json op1 fun_count in
+ let* op2 = operand_of_json op2 fun_count in
Ok (E.BinaryOp (binop, op1, op2))
| `Assoc [ ("Discriminant", place) ] ->
let* place = place_of_json place in
Ok (E.Discriminant place)
| `Assoc [ ("Aggregate", `List [ aggregate_kind; ops ]) ] ->
let* aggregate_kind = aggregate_kind_of_json aggregate_kind in
- let* ops = list_of_json operand_of_json ops in
+ let* ops = list_of_json (fun js -> operand_of_json js fun_count) ops in
Ok (E.Aggregate (aggregate_kind, ops))
| _ -> Error "")
@@ -489,18 +502,18 @@ let fun_id_of_json (js : json) : (A.fun_id, string) result =
combine_error_msgs js "fun_id_of_json"
(match js with
| `Assoc [ ("Regular", id) ] ->
- let* id = A.FunDeclId.id_of_json id in
+ let* id = FunDeclId.id_of_json id in
Ok (A.Regular id)
| `Assoc [ ("Assumed", fid) ] ->
let* fid = assumed_fun_id_of_json fid in
Ok (A.Assumed fid)
| _ -> Error "")
-let assertion_of_json (js : json) : (A.assertion, string) result =
+let assertion_of_json (js : json) (fun_count : int) : (A.assertion, string) result =
combine_error_msgs js "assertion_of_json"
(match js with
| `Assoc [ ("cond", cond); ("expected", expected) ] ->
- let* cond = operand_of_json cond in
+ let* cond = operand_of_json cond fun_count in
let* expected = bool_of_json expected in
Ok { A.cond; expected }
| _ -> Error "")
@@ -534,7 +547,7 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
}
| _ -> Error "")
-let call_of_json (js : json) : (A.call, string) result =
+let call_of_json (js : json) (fun_count : int) : (A.call, string) result =
combine_error_msgs js "call_of_json"
(match js with
| `Assoc
@@ -548,17 +561,17 @@ let call_of_json (js : json) : (A.call, string) result =
let* func = fun_id_of_json func in
let* region_args = list_of_json erased_region_of_json region_args in
let* type_args = list_of_json ety_of_json type_args in
- let* args = list_of_json operand_of_json args in
+ let* args = list_of_json (fun js -> operand_of_json js fun_count) args in
let* dest = place_of_json dest in
Ok { A.func; region_args; type_args; args; dest }
| _ -> Error "")
-let rec statement_of_json (js : json) : (A.statement, string) result =
+let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string) result =
combine_error_msgs js "statement_of_json"
(match js with
| `Assoc [ ("Assign", `List [ place; rvalue ]) ] ->
let* place = place_of_json place in
- let* rvalue = rvalue_of_json rvalue in
+ let* rvalue = rvalue_of_json rvalue fun_count in
Ok (A.Assign (place, rvalue))
| `Assoc [ ("FakeRead", place) ] ->
let* place = place_of_json place in
@@ -571,10 +584,10 @@ let rec statement_of_json (js : json) : (A.statement, string) result =
let* place = place_of_json place in
Ok (A.Drop place)
| `Assoc [ ("Assert", assertion) ] ->
- let* assertion = assertion_of_json assertion in
+ let* assertion = assertion_of_json assertion fun_count in
Ok (A.Assert assertion)
| `Assoc [ ("Call", call) ] ->
- let* call = call_of_json call in
+ let* call = call_of_json call fun_count in
Ok (A.Call call)
| `String "Panic" -> Ok A.Panic
| `String "Return" -> Ok A.Return
@@ -586,47 +599,48 @@ let rec statement_of_json (js : json) : (A.statement, string) result =
Ok (A.Continue i)
| `String "Nop" -> Ok A.Nop
| `Assoc [ ("Sequence", `List [ st1; st2 ]) ] ->
- let* st1 = statement_of_json st1 in
- let* st2 = statement_of_json st2 in
+ let* st1 = statement_of_json st1 fun_count in
+ let* st2 = statement_of_json st2 fun_count 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 in
+ let* op = operand_of_json op fun_count in
+ let* tgt = switch_targets_of_json tgt fun_count in
Ok (A.Switch (op, tgt))
| `Assoc [ ("Loop", st) ] ->
- let* st = statement_of_json st in
+ let* st = statement_of_json st fun_count in
Ok (A.Loop st)
| _ -> Error "")
-and switch_targets_of_json (js : json) : (A.switch_targets, string) result =
+and switch_targets_of_json (js : json) (fun_count : int) : (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 in
- let* st2 = statement_of_json st2 in
+ let* st1 = statement_of_json st1 fun_count in
+ let* st2 = statement_of_json st2 fun_count 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 scalar_value_of_json) statement_of_json)
+ list_of_json (pair_of_json
+ (list_of_json scalar_value_of_json)
+ (fun js -> statement_of_json js fun_count))
tgts
in
- let* otherwise = statement_of_json otherwise in
+ let* otherwise = statement_of_json otherwise fun_count in
Ok (A.SwitchInt (int_ty, tgts, otherwise))
| _ -> Error "")
-let fun_body_of_json (js : json) : (A.fun_body, string) result =
+let fun_body_of_json (js : json) (fun_count : int) : (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 in
+ let* body = statement_of_json body fun_count in
Ok { A.arg_count; locals; body }
| _ -> Error "")
-let fun_decl_of_json (js : json) : (A.fun_decl, string) result =
+let fun_decl_of_json (js : json) (fun_count : int) : (A.fun_decl, string) result =
combine_error_msgs js "fun_decl_of_json"
(match js with
| `Assoc
@@ -636,11 +650,42 @@ let fun_decl_of_json (js : json) : (A.fun_decl, string) result =
("signature", signature);
("body", body);
] ->
- let* def_id = A.FunDeclId.id_of_json def_id in
+ let* def_id = 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_body_of_json body in
- Ok { A.def_id; name; signature; body }
+ let* body = option_of_json (fun js -> fun_body_of_json js fun_count) body in
+ Ok { A.def_id; name; signature; body; is_global = false; }
+ | _ -> Error "")
+
+
+(* Converts a global declaration to a function declaration.
+
+A.fun_sig
+ety_no_regions_to_rty
+*)
+let global_decl_of_json (js : json) (fun_count: int) : (A.fun_decl, string) result =
+ combine_error_msgs js "global_decl_of_json"
+ (match js with
+ | `Assoc
+ [
+ ("def_id", def_id);
+ ("name", name);
+ ("type_", type_);
+ ("body", body);
+ ] ->
+ let* def_id = global_id_of_json def_id fun_count in
+ let* name = fun_name_of_json name in
+ let* type_ = ety_of_json type_ in
+ let* body = option_of_json (fun js -> fun_body_of_json js fun_count) body in
+ let signature : A.fun_sig = {
+ region_params = [];
+ num_early_bound_regions = 0;
+ regions_hierarchy = [];
+ type_params = [];
+ inputs = [];
+ output = TU.ety_no_regions_to_sty type_;
+ } in
+ Ok { A.def_id; name; signature; body; is_global = true; }
| _ -> Error "")
let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
@@ -663,9 +708,14 @@ let type_declaration_group_of_json (js : json) :
let fun_declaration_group_of_json (js : json) :
(M.fun_declaration_group, string) result =
combine_error_msgs js "fun_declaration_group_of_json"
- (g_declaration_group_of_json A.FunDeclId.id_of_json js)
+ (g_declaration_group_of_json FunDeclId.id_of_json js)
+
+let global_declaration_group_of_json (js : json) (fun_count: int) :
+ (M.fun_declaration_group, string) result =
+ combine_error_msgs js "global_declaration_group_of_json"
+ (g_declaration_group_of_json (fun js -> global_id_of_json js fun_count) js)
-let declaration_group_of_json (js : json) : (M.declaration_group, string) result
+let declaration_group_of_json (js : json) (fun_count: int) : (M.declaration_group, string) result
=
combine_error_msgs js "declaration_of_json"
(match js with
@@ -675,8 +725,17 @@ let declaration_group_of_json (js : json) : (M.declaration_group, string) result
| `Assoc [ ("Fun", `List [ decl ]) ] ->
let* decl = fun_declaration_group_of_json decl in
Ok (M.Fun decl)
+ | `Assoc [ ("Global", `List [ decl ]) ] ->
+ let* decl = global_declaration_group_of_json decl fun_count in
+ Ok (M.Fun decl)
| _ -> Error "")
+let length_of_json_list (js: json) : (int, string) result =
+ combine_error_msgs js "get_json_list_len"
+ (match js with
+ | `List jsl -> Ok (List.length jsl)
+ | _ -> Error ("not a list: " ^ show js))
+
let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
combine_error_msgs js "llbc_module_of_json"
(match js with
@@ -686,12 +745,15 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
("declarations", declarations);
("types", types);
("functions", functions);
+ ("globals", globals);
] ->
+ let* fun_count = length_of_json_list functions in
let* name = string_of_json name in
let* declarations =
- list_of_json declaration_group_of_json declarations
+ list_of_json (fun js -> declaration_group_of_json js fun_count) declarations
in
let* types = list_of_json type_decl_of_json types in
- let* functions = list_of_json fun_decl_of_json functions in
- Ok { M.name; declarations; types; functions }
+ let* functions = list_of_json (fun js -> fun_decl_of_json js fun_count) functions in
+ let* globals = list_of_json (fun js -> global_decl_of_json js fun_count) globals in
+ Ok { M.name; declarations; types; functions = functions @ globals }
| _ -> Error "")
diff --git a/src/Modules.ml b/src/Modules.ml
index f52983c6..6d0cf70c 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -1,5 +1,6 @@
open Types
open LlbcAst
+open FunIdentifier
type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
[@@deriving show]
diff --git a/src/Print.ml b/src/Print.ml
index 8e29bc67..28040181 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -1,4 +1,5 @@
open Names
+open FunIdentifier
module T = Types
module TU = TypesUtils
module V = Values
@@ -685,7 +686,7 @@ module LlbcAst = struct
var_id_to_string : V.VarId.id -> string;
adt_field_names :
T.TypeDeclId.id -> T.VariantId.id option -> string list option;
- fun_decl_id_to_string : A.FunDeclId.id -> string;
+ fun_decl_id_to_string : FunDeclId.id -> string;
}
let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter =
@@ -755,7 +756,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) (fdef : A.fun_decl) :
+ (fun_decls : A.fun_decl FunDeclId.Map.t) (fdef : A.fun_decl) :
ast_formatter =
let rvar_to_string r =
let rvar = T.RegionVarId.nth fdef.signature.region_params r in
@@ -781,7 +782,7 @@ module LlbcAst = struct
let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_decls in
let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_decls in
let fun_decl_id_to_string def_id =
- let def = A.FunDeclId.Map.find def_id fun_decls in
+ let def = FunDeclId.Map.find def_id fun_decls in
fun_name_to_string def.name
in
{
@@ -1138,7 +1139,7 @@ module Module = struct
(** Generate an [ast_formatter] by using a definition context in combination
with the variables local to a function's definition *)
let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t)
- (fun_context : A.fun_decl A.FunDeclId.Map.t) (def : A.fun_decl) :
+ (fun_context : A.fun_decl FunDeclId.Map.t) (def : A.fun_decl) :
PA.ast_formatter =
let rvar_to_string vid =
let var = T.RegionVarId.nth def.signature.region_params vid in
@@ -1157,7 +1158,7 @@ module Module = struct
name_to_string def.name
in
let fun_decl_id_to_string def_id =
- let def = A.FunDeclId.Map.find def_id fun_context in
+ let def = FunDeclId.Map.find def_id fun_context in
fun_name_to_string def.name
in
let var_id_to_string vid =
@@ -1186,7 +1187,7 @@ module Module = struct
(** This function pretty-prints a function definition by using a definition
context *)
let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t)
- (fun_context : A.fun_decl A.FunDeclId.Map.t) (def : A.fun_decl) : string =
+ (fun_context : A.fun_decl FunDeclId.Map.t) (def : A.fun_decl) : string =
let fmt = def_ctx_to_ast_formatter type_context fun_context def in
PA.fun_decl_to_string fmt "" " " def
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 5e817dde..8864dafe 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -2,6 +2,7 @@
open Pure
open PureUtils
+open FunIdentifier
module T = Types
module V = Values
module E = Expressions
@@ -12,7 +13,6 @@ module RegionId = T.RegionId
module VariantId = T.VariantId
module FieldId = T.FieldId
module SymbolicValueId = V.SymbolicValueId
-module FunDeclId = A.FunDeclId
type type_formatter = {
type_var_id_to_string : TypeVarId.id -> string;
@@ -44,7 +44,7 @@ type ast_formatter = {
adt_field_to_string :
TypeDeclId.id -> VariantId.id option -> FieldId.id -> string option;
adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option;
- fun_decl_id_to_string : A.FunDeclId.id -> string;
+ fun_decl_id_to_string : FunDeclId.id -> string;
}
let ast_to_value_formatter (fmt : ast_formatter) : value_formatter =
@@ -110,7 +110,7 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
Print.LlbcAst.type_ctx_to_adt_field_to_string_fun type_decls
in
let fun_decl_id_to_string def_id =
- let def = A.FunDeclId.Map.find def_id fun_decls in
+ let def = FunDeclId.Map.find def_id fun_decls in
fun_name_to_string def.name
in
{
diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml
index 0ab68efc..e44b422a 100644
--- a/src/PrintSymbolicAst.ml
+++ b/src/PrintSymbolicAst.ml
@@ -7,6 +7,7 @@
open Errors
open Identifiers
+open FunIdentifier
module T = Types
module TU = TypesUtils
module V = Values
@@ -20,7 +21,7 @@ module PT = Print.Types
type formatting_ctx = {
type_context : C.type_context;
- fun_context : A.fun_decl A.FunDeclId.Map.t;
+ fun_context : A.fun_decl FunDeclId.Map.t;
type_vars : T.type_var list;
}
diff --git a/src/Pure.ml b/src/Pure.ml
index 5834b87f..05f78e35 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -1,5 +1,6 @@
open Identifiers
open Names
+open FunIdentifier
module T = Types
module V = Values
module E = Expressions
@@ -10,7 +11,6 @@ module RegionGroupId = T.RegionGroupId
module VariantId = T.VariantId
module FieldId = T.FieldId
module SymbolicValueId = V.SymbolicValueId
-module FunDeclId = A.FunDeclId
module SynthPhaseId = IdGen ()
(** We give an identifier to every phase of the synthesis (forward, backward
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 1c530011..55a8853a 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -6,6 +6,7 @@
open Pure
open TranslateCore
+open FunIdentifier
module C = Contexts
module RegionVarId = T.RegionVarId
module F = Format
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 42479a6e..2b416cc1 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -2,6 +2,7 @@ open Errors
open LlbcAstUtils
open Pure
open PureUtils
+open FunIdentifier
module Id = Identifiers
module M = Modules
module S = SymbolicAst
diff --git a/src/Translate.ml b/src/Translate.ml
index 57b92e44..1577753c 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -1,5 +1,6 @@
open InterpreterStatements
open Interpreter
+open FunIdentifier
module L = Logging
module T = Types
module A = LlbcAst
@@ -351,8 +352,8 @@ type gen_ctx = {
m : M.llbc_module;
extract_ctx : PureToExtract.extraction_ctx;
trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
- trans_funs : (bool * pure_fun_translation) Pure.FunDeclId.Map.t;
- functions_with_decreases_clause : Pure.FunDeclId.Set.t;
+ trans_funs : (bool * pure_fun_translation) FunDeclId.Map.t;
+ functions_with_decreases_clause : FunDeclId.Set.t;
}
(** Extraction context *)
@@ -388,7 +389,7 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
ctx.trans_types
in
let has_opaque_funs =
- Pure.FunDeclId.Map.exists
+ FunDeclId.Map.exists
(fun _ ((_, (t_fwd, _)) : bool * pure_fun_translation) ->
Option.is_none t_fwd.body)
ctx.trans_funs
@@ -427,7 +428,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
(* Utility to check a function has a decrease clause *)
let has_decreases_clause (def : Pure.fun_decl) : bool =
- Pure.FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause
+ FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause
in
(* In case of (non-mutually) recursive functions, we use a simple procedure to
@@ -523,14 +524,14 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
ids
| Fun (NonRec id) ->
(* Lookup *)
- let pure_fun = Pure.FunDeclId.Map.find id ctx.trans_funs in
+ let pure_fun = FunDeclId.Map.find id ctx.trans_funs in
(* Translate *)
export_functions false [ pure_fun ]
| Fun (Rec ids) ->
(* General case of mutually recursive functions *)
(* Lookup *)
let pure_funs =
- List.map (fun id -> Pure.FunDeclId.Map.find id ctx.trans_funs) ids
+ List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids
in
(* Translate *)
export_functions true pure_funs
@@ -622,7 +623,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
(* We need to compute which functions are recursive, in order to know
* whether we should generate a decrease clause or not. *)
let rec_functions =
- Pure.FunDeclId.Set.of_list
+ FunDeclId.Set.of_list
(List.concat
(List.map
(fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> [])
@@ -644,7 +645,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
(fun ctx (keep_fwd, def) ->
(* Note that we generate a decrease clause for all the recursive functions *)
let gen_decr_clause =
- Pure.FunDeclId.Set.mem (fst def).Pure.def_id rec_functions
+ FunDeclId.Set.mem (fst def).Pure.def_id rec_functions
in
ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd
gen_decr_clause def)
@@ -674,7 +675,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
(List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types)
in
let trans_funs =
- Pure.FunDeclId.Map.of_list
+ FunDeclId.Map.of_list
(List.map
(fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) ->
(fd.def_id, (keep_fwd, (fd, bdl))))
@@ -761,7 +762,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
(* Extract the template clauses *)
let needs_clauses_module =
config.extract_decreases_clauses
- && not (Pure.FunDeclId.Set.is_empty rec_functions)
+ && not (FunDeclId.Set.is_empty rec_functions)
in
(if needs_clauses_module && config.extract_template_decreases_clauses then
let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index 17c35cbf..3d3887ce 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -1,6 +1,7 @@
(** Some utilities for the translation *)
open InterpreterStatements
+open FunIdentifier
module L = Logging
module T = Types
module A = LlbcAst
@@ -14,8 +15,8 @@ let log = L.translate_log
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;
+ fun_decls : A.fun_decl FunDeclId.Map.t;
+ fun_infos : FA.fun_info FunDeclId.Map.t;
}
[@@deriving show]
@@ -49,6 +50,6 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
PrintPure.fun_decl_to_string fmt def
-let fun_decl_id_to_string (ctx : trans_ctx) (id : Pure.FunDeclId.id) : string =
+let fun_decl_id_to_string (ctx : trans_ctx) (id : FunDeclId.id) : string =
Print.fun_name_to_string
- (Pure.FunDeclId.Map.find id ctx.fun_context.fun_decls).name
+ (FunDeclId.Map.find id ctx.fun_context.fun_decls).name
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index bee7956e..8d0624ee 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -100,28 +100,31 @@ let rty_regions_intersect (ty : rty) (regions : RegionId.Set.t) : bool =
let ty_regions = rty_regions ty in
not (RegionId.Set.disjoint ty_regions regions)
-(** Convert an [ety], containing no region variables, to an [rty].
+(** Convert an [ety], containing no region variables, to an [rty] or [sty].
In practice, it is the identity.
*)
-let rec ety_no_regions_to_rty (ty : ety) : rty =
+let rec ety_no_regions_to_gr_ty (ty : ety) : 'a gr_ty =
match ty with
| Adt (type_id, regions, tys) ->
assert (regions = []);
- Adt (type_id, [], List.map ety_no_regions_to_rty tys)
+ Adt (type_id, [], List.map ety_no_regions_to_gr_ty tys)
| TypeVar v -> TypeVar v
| Bool -> Bool
| Char -> Char
| Never -> Never
| Integer int_ty -> Integer int_ty
| Str -> Str
- | Array ty -> Array (ety_no_regions_to_rty ty)
- | Slice ty -> Slice (ety_no_regions_to_rty ty)
+ | Array ty -> Array (ety_no_regions_to_gr_ty ty)
+ | Slice ty -> Slice (ety_no_regions_to_gr_ty ty)
| Ref (_, _, _) ->
failwith
"Can't convert a ref with erased regions to a ref with non-erased \
regions"
+let ety_no_regions_to_rty (ty : ety) : rty = ety_no_regions_to_gr_ty ty
+let ety_no_regions_to_sty (ty : ety) : sty = ety_no_regions_to_gr_ty ty
+
(** Retuns true if the type contains borrows.
Note that we can't simply explore the type and look for regions: sometimes
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 06:36:59 +0000