summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Assumed.ml2
-rw-r--r--src/CfimOfJson.ml8
-rw-r--r--src/Contexts.ml2
-rw-r--r--src/Interpreter.ml14
-rw-r--r--src/InterpreterStatements.ml2
-rw-r--r--src/InterpreterUtils.ml4
-rw-r--r--src/Invariants.ml2
-rw-r--r--src/LlbcAst.ml (renamed from src/CfimAst.ml)0
-rw-r--r--src/LlbcAstUtils.ml (renamed from src/CfimAstUtils.ml)2
-rw-r--r--src/Logging.ml2
-rw-r--r--src/Modules.ml6
-rw-r--r--src/PrePasses.ml4
-rw-r--r--src/Print.ml10
-rw-r--r--src/PrintPure.ml6
-rw-r--r--src/PrintSymbolicAst.ml2
-rw-r--r--src/Pure.ml2
-rw-r--r--src/PureMicroPasses.ml4
-rw-r--r--src/PureToExtract.ml4
-rw-r--r--src/Substitute.ml2
-rw-r--r--src/SymbolicAst.ml2
-rw-r--r--src/SymbolicToPure.ml38
-rw-r--r--src/SynthesizeSymbolic.ml2
-rw-r--r--src/Translate.ml18
-rw-r--r--src/TranslateCore.ml2
-rw-r--r--src/main.ml8
25 files changed, 74 insertions, 74 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml
index 6f53c302..8ce518c9 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -32,7 +32,7 @@
open Names
open TypesUtils
module T = Types
-module A = CfimAst
+module A = LlbcAst
module Sig = struct
(** A few utilities *)
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index 43ca1074..e293b030 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -16,10 +16,10 @@ module V = Values
module S = Scalars
module M = Modules
module E = Expressions
-module A = CfimAst
+module A = LlbcAst
(* The default logger *)
-let log = Logging.cfim_of_json_logger
+let log = Logging.llbc_of_json_logger
let path_elem_of_json (js : json) : (path_elem, string) result =
combine_error_msgs js "path_elem_of_json"
@@ -662,8 +662,8 @@ let declaration_group_of_json (js : json) : (M.declaration_group, string) result
Ok (M.Fun decl)
| _ -> Error "")
-let cfim_module_of_json (js : json) : (M.cfim_module, string) result =
- combine_error_msgs js "cfim_module_of_json"
+let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
+ combine_error_msgs js "llbc_module_of_json"
(match js with
| `Assoc
[
diff --git a/src/Contexts.ml b/src/Contexts.ml
index b5431f0f..1fb8cac1 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -1,6 +1,6 @@
open Types
open Values
-open CfimAst
+open LlbcAst
module V = Values
open ValuesUtils
module M = Modules
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index d073c238..82eb4b35 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -3,17 +3,17 @@ open InterpreterUtils
open InterpreterProjectors
open InterpreterBorrows
open InterpreterStatements
-open CfimAstUtils
+open LlbcAstUtils
module L = Logging
module T = Types
-module A = CfimAst
+module A = LlbcAst
module M = Modules
module SA = SymbolicAst
(** The local logger *)
let log = L.interpreter_log
-let compute_type_fun_contexts (m : M.cfim_module) :
+let compute_type_fun_contexts (m : M.llbc_module) :
C.type_context * C.fun_context =
let type_decls_list, _ = M.split_declarations m.declarations in
let type_decls, fun_decls = M.compute_defs_maps m in
@@ -251,7 +251,7 @@ module Test = struct
(** Test a unit function (taking no arguments) by evaluating it in an empty
environment.
*)
- let test_unit_function (config : C.partial_config) (m : M.cfim_module)
+ let test_unit_function (config : C.partial_config) (m : M.llbc_module)
(fid : A.FunDeclId.id) : unit =
(* Retrieve the function declaration *)
let fdef = A.FunDeclId.nth m.functions fid in
@@ -298,7 +298,7 @@ module Test = struct
&& List.length def.A.signature.inputs = 0
(** Test all the unit functions in a list of function definitions *)
- let test_unit_functions (config : C.partial_config) (m : M.cfim_module) : unit
+ let test_unit_functions (config : C.partial_config) (m : M.llbc_module) : unit
=
let unit_funs = List.filter fun_decl_is_unit m.functions in
let test_unit_fun (def : A.fun_decl) : unit =
@@ -335,9 +335,9 @@ module Test = struct
they are not supported by the symbolic interpreter.
*)
let test_functions_symbolic (config : C.partial_config) (synthesize : bool)
- (m : M.cfim_module) : unit =
+ (m : M.llbc_module) : unit =
let no_loop_funs =
- List.filter (fun f -> not (CfimAstUtils.fun_decl_has_loops f)) m.functions
+ List.filter (fun f -> not (LlbcAstUtils.fun_decl_has_loops f)) m.functions
in
let type_context, fun_context = compute_type_fun_contexts m in
let test_fun (def : A.fun_decl) : unit =
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index dc8fc7f7..547f5ee3 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -3,7 +3,7 @@ module V = Values
module E = Expressions
module C = Contexts
module Subst = Substitute
-module A = CfimAst
+module A = LlbcAst
module L = Logging
open TypesUtils
open ValuesUtils
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 68547d86..27d65a62 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -3,11 +3,11 @@ module V = Values
module E = Expressions
module C = Contexts
module Subst = Substitute
-module A = CfimAst
+module A = LlbcAst
module L = Logging
open Utils
open TypesUtils
-module PA = Print.EvalCtxCfimAst
+module PA = Print.EvalCtxLlbcAst
(** Some utilities *)
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 78d7cb8d..f12911d4 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -6,7 +6,7 @@ module V = Values
module E = Expressions
module C = Contexts
module Subst = Substitute
-module A = CfimAst
+module A = LlbcAst
module L = Logging
open Cps
open TypesUtils
diff --git a/src/CfimAst.ml b/src/LlbcAst.ml
index f597cd27..f597cd27 100644
--- a/src/CfimAst.ml
+++ b/src/LlbcAst.ml
diff --git a/src/CfimAstUtils.ml b/src/LlbcAstUtils.ml
index 57906143..93ca4448 100644
--- a/src/CfimAstUtils.ml
+++ b/src/LlbcAstUtils.ml
@@ -1,4 +1,4 @@
-open CfimAst
+open LlbcAst
open Utils
module T = Types
diff --git a/src/Logging.ml b/src/Logging.ml
index 7067920b..7f4152a5 100644
--- a/src/Logging.ml
+++ b/src/Logging.ml
@@ -10,7 +10,7 @@ let main_log = L.get_logger "MainLogger"
toggle logging on/off, depending on which information we need *)
(** Logger for CfimOfJson *)
-let cfim_of_json_logger = L.get_logger "MainLogger.CfimOfJson"
+let llbc_of_json_logger = L.get_logger "MainLogger.CfimOfJson"
(** Logger for PrePasses *)
let pre_passes_log = L.get_logger "MainLogger.PrePasses"
diff --git a/src/Modules.ml b/src/Modules.ml
index 3ee4c9ed..f52983c6 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -1,5 +1,5 @@
open Types
-open CfimAst
+open LlbcAst
type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
[@@deriving show]
@@ -15,7 +15,7 @@ type declaration_group =
| Fun of fun_declaration_group
[@@deriving show]
-type cfim_module = {
+type llbc_module = {
name : string;
declarations : declaration_group list;
types : type_decl list;
@@ -23,7 +23,7 @@ type cfim_module = {
}
(** LLBC module - TODO: rename to crate *)
-let compute_defs_maps (m : cfim_module) :
+let compute_defs_maps (m : llbc_module) :
type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t =
let types_map =
List.fold_left
diff --git a/src/PrePasses.ml b/src/PrePasses.ml
index 925b82aa..9b1a6990 100644
--- a/src/PrePasses.ml
+++ b/src/PrePasses.ml
@@ -6,7 +6,7 @@ module T = Types
module V = Values
module E = Expressions
module C = Contexts
-module A = CfimAst
+module A = LlbcAst
module M = Modules
module L = Logging
@@ -45,6 +45,6 @@ let filter_drop_assigns (f : A.fun_decl) : A.fun_decl =
let body = obj#visit_statement () f.body in
{ f with body }
-let apply_passes (m : M.cfim_module) : M.cfim_module =
+let apply_passes (m : M.llbc_module) : M.llbc_module =
let functions = List.map filter_drop_assigns m.functions in
{ m with functions }
diff --git a/src/Print.ml b/src/Print.ml
index c3c80da0..18227c61 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -4,7 +4,7 @@ module TU = TypesUtils
module V = Values
module VU = ValuesUtils
module E = Expressions
-module A = CfimAst
+module A = LlbcAst
module C = Contexts
module M = Modules
@@ -677,7 +677,7 @@ end
module PC = Contexts (* local module *)
(** Pretty-printing for contexts (generic functions) *)
-module CfimAst = struct
+module LlbcAst = struct
let var_to_string (var : A.var) : string =
match var.name with
| None -> V.VarId.to_string var.index
@@ -1099,7 +1099,7 @@ module CfimAst = struct
^ "\n\n" ^ body ^ "\n" ^ indent ^ "}"
end
-module PA = CfimAst (* local module *)
+module PA = LlbcAst (* local module *)
(** Pretty-printing for ASTs (functions based on a definition context) *)
module Module = struct
@@ -1168,7 +1168,7 @@ module Module = struct
let fmt = def_ctx_to_ast_formatter type_context fun_context def in
PA.fun_decl_to_string fmt "" " " def
- let module_to_string (m : M.cfim_module) : string =
+ let module_to_string (m : M.llbc_module) : string =
let types_defs_map, funs_defs_map = M.compute_defs_maps m in
(* The types *)
@@ -1185,7 +1185,7 @@ module Module = struct
end
(** Pretty-printing for CFIM ASTs (functions based on an evaluation context) *)
-module EvalCtxCfimAst = struct
+module EvalCtxLlbcAst = struct
let ety_to_string (ctx : C.eval_ctx) (t : T.ety) : string =
let fmt = PC.eval_ctx_to_ctx_formatter ctx in
let fmt = PC.ctx_to_etype_formatter fmt in
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 65b151a3..f47a1f06 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -4,7 +4,7 @@ open Pure
module T = Types
module V = Values
module E = Expressions
-module A = CfimAst
+module A = LlbcAst
module TypeDeclId = T.TypeDeclId
module TypeVarId = T.TypeVarId
module RegionId = T.RegionId
@@ -111,7 +111,7 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
Print.Contexts.type_ctx_to_adt_field_names_fun type_decls
in
let adt_field_to_string =
- Print.CfimAst.type_ctx_to_adt_field_to_string_fun type_decls
+ 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
@@ -383,7 +383,7 @@ let fun_suffix (rg_id : T.RegionGroupId.id option) : string =
let unop_to_string (unop : unop) : string =
match unop with Not -> "¬" | Neg _ -> "-"
-let binop_to_string = Print.CfimAst.binop_to_string
+let binop_to_string = Print.LlbcAst.binop_to_string
let fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string =
match fun_id with
diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml
index 1679aa6c..0ab68efc 100644
--- a/src/PrintSymbolicAst.ml
+++ b/src/PrintSymbolicAst.ml
@@ -11,7 +11,7 @@ module T = Types
module TU = TypesUtils
module V = Values
module E = Expressions
-module A = CfimAst
+module A = LlbcAst
module C = Contexts
module M = Modules
open SymbolicAst
diff --git a/src/Pure.ml b/src/Pure.ml
index 422292b1..a4b193f7 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -3,7 +3,7 @@ open Names
module T = Types
module V = Values
module E = Expressions
-module A = CfimAst
+module A = LlbcAst
module TypeDeclId = T.TypeDeclId
module TypeVarId = T.TypeVarId
module RegionGroupId = T.RegionGroupId
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index c1cacac5..b110f829 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -504,11 +504,11 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) (call0 : call)
(* We need to use the regions hierarchy *)
(* First, lookup the signature of the CFIM function *)
let sg =
- CfimAstUtils.lookup_fun_sig id0 ctx.fun_context.fun_decls
+ LlbcAstUtils.lookup_fun_sig id0 ctx.fun_context.fun_decls
in
(* Compute the set of ancestors of the function in call1 *)
let call1_ancestors =
- CfimAstUtils.list_parent_region_groups sg rg_id1
+ LlbcAstUtils.list_parent_region_groups sg rg_id1
in
(* Check if the function used in call0 is inside *)
T.RegionGroupId.Set.mem rg_id0 call1_ancestors
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 2a00577e..8a2b2aa3 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -572,10 +572,10 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
(def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
(* Lookup the CFIM def to compute the region group information *)
let def_id = def.def_id in
- let cfim_def =
+ let llbc_def =
FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls
in
- let sg = cfim_def.signature in
+ let sg = llbc_def.signature in
let num_rgs = List.length sg.regions_hierarchy in
let keep_fwd, (_, backs) = trans_group in
let num_backs = List.length backs in
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 0bc612ea..10d6d419 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -6,7 +6,7 @@ module T = Types
module TU = TypesUtils
module V = Values
module E = Expressions
-module A = CfimAst
+module A = LlbcAst
module C = Contexts
(** Substitute types variables and regions in a type.
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index aad5de15..3df91d23 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -6,7 +6,7 @@
module T = Types
module V = Values
module E = Expressions
-module A = CfimAst
+module A = LlbcAst
type mplace = {
bv : Contexts.binder;
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 18b8f507..fd41f094 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1,5 +1,5 @@
open Errors
-open CfimAstUtils
+open LlbcAstUtils
open Pure
open PureUtils
module Id = Identifiers
@@ -41,7 +41,7 @@ type config = {
}
type type_context = {
- cfim_type_decls : T.type_decl TypeDeclId.Map.t;
+ llbc_type_decls : T.type_decl TypeDeclId.Map.t;
type_decls : type_decl TypeDeclId.Map.t;
(** We use this for type-checking (for sanity checks) when translating
values and functions.
@@ -66,7 +66,7 @@ type fun_sig_named_outputs = {
}
type fun_context = {
- cfim_fun_decls : A.fun_decl FunDeclId.Map.t;
+ llbc_fun_decls : A.fun_decl FunDeclId.Map.t;
fun_sigs : fun_sig_named_outputs RegularFunIdMap.t; (** *)
}
@@ -114,14 +114,14 @@ let type_check_lvalue (ctx : bs_ctx) (v : typed_lvalue) : unit =
TypeCheck.check_typed_lvalue ctx v
(* TODO: move *)
-let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.CfimAst.ast_formatter =
- Print.CfimAst.fun_decl_to_ast_formatter ctx.type_context.cfim_type_decls
- ctx.fun_context.cfim_fun_decls ctx.fun_decl
+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 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.cfim_type_decls in
- let fun_decls = ctx.fun_context.cfim_fun_decls in
+ let type_decls = ctx.type_context.llbc_type_decls in
+ let fun_decls = ctx.fun_context.llbc_fun_decls in
PrintPure.mk_ast_formatter type_decls fun_decls type_params
let ty_to_string (ctx : bs_ctx) (ty : ty) : string =
@@ -131,7 +131,7 @@ let ty_to_string (ctx : bs_ctx) (ty : ty) : string =
let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
let type_params = def.type_params in
- let type_decls = ctx.type_context.cfim_type_decls in
+ let type_decls = ctx.type_context.llbc_type_decls in
let fmt = PrintPure.mk_type_formatter type_decls type_params in
PrintPure.type_decl_to_string fmt def
@@ -141,22 +141,22 @@ let typed_rvalue_to_string (ctx : bs_ctx) (v : typed_rvalue) : string =
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.cfim_type_decls in
- let fun_decls = ctx.fun_context.cfim_fun_decls in
+ let type_decls = ctx.type_context.llbc_type_decls in
+ let fun_decls = ctx.fun_context.llbc_fun_decls in
let fmt = PrintPure.mk_ast_formatter type_decls fun_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.cfim_type_decls in
- let fun_decls = ctx.fun_context.cfim_fun_decls in
+ let type_decls = ctx.type_context.llbc_type_decls in
+ let fun_decls = ctx.fun_context.llbc_fun_decls in
let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
PrintPure.fun_decl_to_string fmt def
(* 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.CfimAst.ast_to_value_formatter fmt in
+ let fmt = Print.LlbcAst.ast_to_value_formatter fmt in
let indent = "" in
let indent_incr = " " in
Print.Values.abs_to_string fmt indent indent_incr abs
@@ -173,13 +173,13 @@ let get_instantiated_fun_sig (fun_id : A.fun_id)
(* Apply *)
fun_sig_substitute tsubst sg
-let bs_ctx_lookup_cfim_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
+let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
T.type_decl =
- TypeDeclId.Map.find id ctx.type_context.cfim_type_decls
+ TypeDeclId.Map.find id ctx.type_context.llbc_type_decls
-let bs_ctx_lookup_cfim_fun_decl (id : FunDeclId.id) (ctx : bs_ctx) : A.fun_decl
+let bs_ctx_lookup_llbc_fun_decl (id : FunDeclId.id) (ctx : bs_ctx) : A.fun_decl
=
- FunDeclId.Map.find id ctx.fun_context.cfim_fun_decls
+ FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls
(* TODO: move *)
let bs_ctx_lookup_local_function_sig (def_id : FunDeclId.id)
@@ -1294,7 +1294,7 @@ and translate_expansion (config : config) (p : S.mplace option)
match type_id with
| T.AdtId adt_id ->
(* Detect if this is an enumeration or not *)
- let tdef = bs_ctx_lookup_cfim_type_decl adt_id ctx in
+ let tdef = bs_ctx_lookup_llbc_type_decl adt_id ctx in
let is_enum = type_decl_is_enum tdef in
if is_enum then
(* This is an enumeration: introduce an [ExpandEnum] let-binding *)
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index c1dcff87..785f034b 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -2,7 +2,7 @@ module C = Collections
module T = Types
module V = Values
module E = Expressions
-module A = CfimAst
+module A = LlbcAst
open SymbolicAst
let mk_mplace (p : E.place) (ctx : Contexts.eval_ctx) : mplace =
diff --git a/src/Translate.ml b/src/Translate.ml
index 7e4e6178..ce669525 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -2,7 +2,7 @@ open InterpreterStatements
open Interpreter
module L = Logging
module T = Types
-module A = CfimAst
+module A = LlbcAst
module M = Modules
module SA = SymbolicAst
module Micro = PureMicroPasses
@@ -122,12 +122,12 @@ let translate_function_to_pure (config : C.partial_config)
let type_context =
{
SymbolicToPure.types_infos = type_context.type_infos;
- cfim_type_decls = type_context.type_decls;
+ llbc_type_decls = type_context.type_decls;
type_decls = pure_type_decls;
}
in
let fun_context =
- { SymbolicToPure.cfim_fun_decls = fun_context.fun_decls; fun_sigs }
+ { SymbolicToPure.llbc_fun_decls = fun_context.fun_decls; fun_sigs }
in
let ctx =
{
@@ -152,7 +152,7 @@ let translate_function_to_pure (config : C.partial_config)
in
(* We need to initialize the input/output variables *)
- let forward_input_vars = CfimAstUtils.fun_decl_get_input_vars fdef in
+ let forward_input_vars = LlbcAstUtils.fun_decl_get_input_vars fdef in
let forward_input_varnames =
List.map (fun (v : A.var) -> v.name) forward_input_vars
in
@@ -245,7 +245,7 @@ let translate_function_to_pure (config : C.partial_config)
(pure_forward, pure_backwards)
let translate_module_to_pure (config : C.partial_config)
- (mp_config : Micro.config) (m : M.cfim_module) :
+ (mp_config : Micro.config) (m : M.llbc_module) :
trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list =
(* Debug *)
log#ldebug (lazy "translate_module_to_pure");
@@ -276,7 +276,7 @@ let translate_module_to_pure (config : C.partial_config)
( A.Local fdef.def_id,
List.map
(fun (v : A.var) -> v.name)
- (CfimAstUtils.fun_decl_get_input_vars fdef),
+ (LlbcAstUtils.fun_decl_get_input_vars fdef),
fdef.signature ))
m.functions
in
@@ -304,7 +304,7 @@ let translate_module_to_pure (config : C.partial_config)
(trans_ctx, type_decls, pure_translations)
type gen_ctx = {
- m : M.cfim_module;
+ 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;
@@ -514,7 +514,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
(** Translate a module and write the synthesized code to an output file. *)
let translate_module (filename : string) (dest_dir : string) (config : config)
- (m : M.cfim_module) : unit =
+ (m : M.llbc_module) : unit =
(* Translate the module to the pure AST *)
let trans_ctx, trans_types, trans_funs =
translate_module_to_pure config.eval_config config.mp_config m
@@ -568,7 +568,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
(* First compute the filename by replacing the extension and converting the
* case (rust module names are snake case) *)
let module_name, extract_filebasename =
- match Filename.chop_suffix_opt ~suffix:".cfim" filename with
+ match Filename.chop_suffix_opt ~suffix:".llbc" filename with
| None ->
(* Note that we already checked the suffix upon opening the file *)
failwith "Unreachable"
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index 3a22d388..6e5204f6 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -3,7 +3,7 @@
open InterpreterStatements
module L = Logging
module T = Types
-module A = CfimAst
+module A = LlbcAst
module M = Modules
module SA = SymbolicAst
diff --git a/src/main.ml b/src/main.ml
index 15468d6c..4740f14c 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -2,7 +2,7 @@ open CfimOfJson
open Logging
open Print
module T = Types
-module A = CfimAst
+module A = LlbcAst
module I = Interpreter
module EL = Easy_logging.Logging
module TA = TypesAnalysis
@@ -102,7 +102,7 @@ let () =
let filename =
match !filenames with
| [ f ] ->
- if not (Filename.check_suffix f ".cfim") then (
+ if not (Filename.check_suffix f ".llbc") then (
print_string "Unrecognized file extension";
fail ())
else if not (Sys.file_exists f) then (
@@ -123,7 +123,7 @@ let () =
* command-line arguments *)
Easy_logging.Handlers.set_level main_logger_handler EL.Info;
main_log#set_level EL.Info;
- cfim_of_json_logger#set_level EL.Info;
+ llbc_of_json_logger#set_level EL.Info;
pre_passes_log#set_level EL.Info;
interpreter_log#set_level EL.Info;
statements_log#set_level EL.Info;
@@ -139,7 +139,7 @@ let () =
translate_log#set_level EL.Info;
(* Load the module *)
let json = Yojson.Basic.from_file filename in
- match cfim_module_of_json json with
+ match llbc_module_of_json json with
| Error s ->
main_log#error "error: %s\n" s;
exit 1
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 05:51:53 +0000