summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/InterpreterStatements.ml4
-rw-r--r--src/LlbcAst.ml2
-rw-r--r--src/LlbcAstUtils.ml4
-rw-r--r--src/LlbcOfJson.ml4
-rw-r--r--src/Print.ml2
-rw-r--r--src/PrintPure.ml2
-rw-r--r--src/PureMicroPasses.ml4
-rw-r--r--src/PureToExtract.ml12
-rw-r--r--src/PureUtils.ml4
-rw-r--r--src/SymbolicToPure.ml4
-rw-r--r--src/Translate.ml8
-rw-r--r--src/main.ml3
12 files changed, 27 insertions, 26 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 3ea0a6fa..ef7c09e8 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -990,7 +990,7 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
- this is a non-local function, in which case there is a special treatment
*)
match call.func with
- | A.Local fid ->
+ | A.Regular fid ->
eval_local_function_call config fid call.region_params call.type_params
call.args call.dest
| A.Assumed fid ->
@@ -1085,7 +1085,7 @@ and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
(* Sanity check *)
assert (List.length args = List.length def.A.signature.inputs);
(* Evaluate the function call *)
- eval_function_call_symbolic_from_inst_sig config (A.Local fid) inst_sg
+ eval_function_call_symbolic_from_inst_sig config (A.Regular fid) inst_sg
region_params type_params args dest cf ctx
(** Evaluate a function call in symbolic mode by using the function signature.
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index f5ffc956..6e77cadb 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -33,7 +33,7 @@ type assumed_fun_id =
(** `core::ops::index::IndexMut::index_mut<alloc::vec::Vec<T>, usize>` *)
[@@deriving show, ord]
-type fun_id = Local of FunDeclId.id | Assumed of assumed_fun_id
+type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id
[@@deriving show, ord]
type assertion = { cond : operand; expected : bool } [@@deriving show]
diff --git a/src/LlbcAstUtils.ml b/src/LlbcAstUtils.ml
index 41d17bf4..84e8e00f 100644
--- a/src/LlbcAstUtils.ml
+++ b/src/LlbcAstUtils.ml
@@ -25,13 +25,13 @@ let fun_decl_has_loops (fd : fun_decl) : bool =
let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
fun_sig =
match fun_id with
- | Local id -> (FunDeclId.Map.find id fun_decls).signature
+ | Regular id -> (FunDeclId.Map.find id fun_decls).signature
| Assumed aid -> Assumed.get_assumed_sig aid
let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
Names.fun_name =
match fun_id with
- | Local id -> (FunDeclId.Map.find id fun_decls).name
+ | Regular id -> (FunDeclId.Map.find id fun_decls).name
| Assumed aid -> Assumed.get_assumed_name aid
(** Small utility: list the transitive parents of a region var group.
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 6e0adfb6..93ba7696 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -479,9 +479,9 @@ let assumed_fun_id_of_json (js : json) : (A.assumed_fun_id, string) result =
let fun_id_of_json (js : json) : (A.fun_id, string) result =
combine_error_msgs js "fun_id_of_json"
(match js with
- | `Assoc [ ("Local", id) ] ->
+ | `Assoc [ ("Regular", id) ] ->
let* id = A.FunDeclId.id_of_json id in
- Ok (A.Local id)
+ Ok (A.Regular id)
| `Assoc [ ("Assumed", fid) ] ->
let* fid = assumed_fun_id_of_json fid in
Ok (A.Assumed fid)
diff --git a/src/Print.ml b/src/Print.ml
index d2101dae..24945298 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -965,7 +965,7 @@ module LlbcAst = struct
let args = "(" ^ String.concat ", " args ^ ")" in
let name_params =
match call.A.func with
- | A.Local fid -> fmt.fun_decl_id_to_string fid ^ params
+ | A.Regular fid -> fmt.fun_decl_id_to_string fid ^ params
| A.Assumed fid -> (
match fid with
| A.Replace -> "core::mem::replace" ^ params
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 52215019..27e5ff37 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -359,7 +359,7 @@ let inst_fun_sig_to_string (fmt : ast_formatter) (sg : inst_fun_sig) : string =
let regular_fun_id_to_string (fmt : ast_formatter) (fun_id : A.fun_id) : string
=
match fun_id with
- | A.Local fid -> fmt.fun_decl_id_to_string fid
+ | A.Regular fid -> fmt.fun_decl_id_to_string fid
| A.Assumed fid -> (
match fid with
| A.Replace -> "core::mem::replace"
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 5227b2ad..cc661883 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -776,7 +776,7 @@ let to_monadic (config : config) (def : fun_decl) : fun_decl =
method! visit_call env call =
match call.func with
- | Regular (A.Local _, _) ->
+ | Regular (A.Regular _, _) ->
if call.args = [] && config.add_unit_args then
let args = [ mk_value_expression unit_rvalue None ] in
{ call with args }
@@ -1015,7 +1015,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
* it more idiomatic lambda calculus... *)
let re_call_can_use_state =
match re_call.func with
- | Regular (A.Local _, _) -> true
+ | Regular (A.Regular _, _) -> true
| Regular (A.Assumed _, _) | Unop _ | Binop _ -> false
in
if config.use_state_monad && re_call_can_use_state then
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 8a2b2aa3..bbcf2cec 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -355,7 +355,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| FunId (fid, rg_id) ->
let fun_name =
match fid with
- | A.Local fid ->
+ | A.Regular fid ->
Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name
| A.Assumed aid -> A.show_assumed_fun_id aid
in
@@ -368,7 +368,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| DecreasesClauseId fid ->
let fun_name =
match fid with
- | A.Local fid ->
+ | A.Regular fid ->
Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name
| A.Assumed aid -> A.show_assumed_fun_id aid
in
@@ -446,7 +446,7 @@ let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option)
let ctx_get_local_function (id : FunDeclId.id) (rg : RegionGroupId.id option)
(ctx : extraction_ctx) : string =
- ctx_get_function (A.Local id) rg ctx
+ ctx_get_function (A.Regular id) rg ctx
let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string =
assert (id <> Tuple);
@@ -477,7 +477,7 @@ let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id)
let ctx_get_decreases_clause (def_id : FunDeclId.id) (ctx : extraction_ctx) :
string =
- ctx_get (DecreasesClauseId (A.Local def_id)) ctx
+ ctx_get (DecreasesClauseId (A.Regular def_id)) ctx
(** Generate a unique type variable name and add it to the context *)
let ctx_add_type_var (basename : string) (id : TypeVarId.id)
@@ -566,7 +566,7 @@ let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) :
let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
let name = ctx.fmt.decreases_clause_name def.def_id def.basename in
- ctx_add (DecreasesClauseId (A.Local def.def_id)) name ctx
+ ctx_add (DecreasesClauseId (A.Regular def.def_id)) name ctx
let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
(def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
@@ -594,7 +594,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
in
Some { id = rg_id; region_names }
in
- let def_id = A.Local def_id in
+ let def_id = A.Regular def_id in
let name =
ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs)
in
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 2a56b6e0..23bffa1d 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -230,14 +230,14 @@ let functions_not_mutually_recursive (funs : fun_decl list) : bool =
let ids =
FunIdSet.of_list
(List.map
- (fun (f : fun_decl) -> Regular (A.Local f.def_id, f.back_id))
+ (fun (f : fun_decl) -> Regular (A.Regular f.def_id, f.back_id))
funs)
in
let ids = ref ids in
(* Explore every body *)
let body_only_calls_itself (fdef : fun_decl) : bool =
(* Remove the current id from the id set *)
- ids := FunIdSet.remove (Regular (A.Local fdef.def_id, fdef.back_id)) !ids;
+ ids := FunIdSet.remove (Regular (A.Regular fdef.def_id, fdef.back_id)) !ids;
(* Check if we call functions from the updated id set *)
let obj =
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index dbf09e57..fe500480 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -184,7 +184,7 @@ let bs_ctx_lookup_llbc_fun_decl (id : FunDeclId.id) (ctx : bs_ctx) : A.fun_decl
(* TODO: move *)
let bs_ctx_lookup_local_function_sig (def_id : FunDeclId.id)
(back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig =
- let id = (A.Local def_id, back_id) in
+ let id = (A.Regular def_id, back_id) in
(RegularFunIdMap.find id ctx.fun_context.fun_sigs).sg
let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
@@ -942,7 +942,7 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) : S.call * V.abs list =
*)
let fun_is_monadic (fun_id : A.fun_id) : bool =
match fun_id with
- | A.Local _ -> true
+ | A.Regular _ -> true
| A.Assumed aid -> Assumed.assumed_is_monadic aid
let rec translate_expression (config : config) (e : S.expression) (ctx : bs_ctx)
diff --git a/src/Translate.ml b/src/Translate.ml
index 095f2535..e547ad60 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -115,7 +115,7 @@ let translate_function_to_pure (config : C.partial_config)
(* Convert the symbolic ASTs to pure ASTs: *)
(* Initialize the context *)
- let forward_sig = RegularFunIdMap.find (A.Local def_id, None) fun_sigs in
+ let forward_sig = RegularFunIdMap.find (A.Regular def_id, None) fun_sigs in
let forward_ret_ty =
match forward_sig.sg.outputs with
| [ ty ] -> ty
@@ -205,7 +205,7 @@ let translate_function_to_pure (config : C.partial_config)
(* Initialize the context - note that the ret_ty is not really
* useful as we don't translate a body *)
let backward_sg =
- RegularFunIdMap.find (A.Local def_id, Some back_id) fun_sigs
+ RegularFunIdMap.find (A.Regular def_id, Some back_id) fun_sigs
in
let backward_ret_ty = mk_simpl_tuple_ty backward_sg.sg.outputs in
let ctx = { ctx with bid = Some back_id; ret_ty = backward_ret_ty } in
@@ -219,7 +219,7 @@ let translate_function_to_pure (config : C.partial_config)
let ctx = add_forward_inputs input_svs ctx in
(* TODO: the computation of the backward inputs is a bit awckward... *)
let backward_sg =
- RegularFunIdMap.find (A.Local def_id, Some back_id) fun_sigs
+ RegularFunIdMap.find (A.Regular def_id, Some back_id) fun_sigs
in
let _, backward_inputs =
Collections.List.split_at backward_sg.sg.inputs num_forward_inputs
@@ -311,7 +311,7 @@ let translate_module_to_pure (config : C.partial_config)
(fun (v : A.var) -> v.name)
(LlbcAstUtils.fun_body_get_input_vars body)
in
- (A.Local fdef.def_id, input_names, fdef.signature))
+ (A.Regular fdef.def_id, input_names, fdef.signature))
m.functions
in
let sigs = List.append assumed_sigs local_sigs in
diff --git a/src/main.ml b/src/main.ml
index 577ba666..6d4888f9 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -102,7 +102,8 @@ let () =
let filename =
match !filenames with
| [ f ] ->
- if not (Filename.check_suffix f ".llbc") then (
+ (* TODO: update the extension *)
+ if not (Filename.check_suffix f ".cfim") then (
print_string "Unrecognized file extension";
fail ())
else if not (Sys.file_exists f) then (
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 16:54:05 +0000