diff options
author | Son Ho | 2022-03-03 13:20:26 +0100 |
---|---|---|
committer | Son Ho | 2022-03-03 13:20:26 +0100 |
commit | 90195f830788f53d214754a732bd094247a91c70 (patch) | |
tree | 4f5d2c748e61e06008e77430b29e5da513c4b8bd | |
parent | df04dee24f1c83998aa314382f70e3961def8f10 (diff) |
Rename CFIM to LLBC
-rw-r--r-- | src/Assumed.ml | 2 | ||||
-rw-r--r-- | src/CfimOfJson.ml | 8 | ||||
-rw-r--r-- | src/Contexts.ml | 2 | ||||
-rw-r--r-- | src/Interpreter.ml | 14 | ||||
-rw-r--r-- | src/InterpreterStatements.ml | 2 | ||||
-rw-r--r-- | src/InterpreterUtils.ml | 4 | ||||
-rw-r--r-- | src/Invariants.ml | 2 | ||||
-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.ml | 2 | ||||
-rw-r--r-- | src/Modules.ml | 6 | ||||
-rw-r--r-- | src/PrePasses.ml | 4 | ||||
-rw-r--r-- | src/Print.ml | 10 | ||||
-rw-r--r-- | src/PrintPure.ml | 6 | ||||
-rw-r--r-- | src/PrintSymbolicAst.ml | 2 | ||||
-rw-r--r-- | src/Pure.ml | 2 | ||||
-rw-r--r-- | src/PureMicroPasses.ml | 4 | ||||
-rw-r--r-- | src/PureToExtract.ml | 4 | ||||
-rw-r--r-- | src/Substitute.ml | 2 | ||||
-rw-r--r-- | src/SymbolicAst.ml | 2 | ||||
-rw-r--r-- | src/SymbolicToPure.ml | 38 | ||||
-rw-r--r-- | src/SynthesizeSymbolic.ml | 2 | ||||
-rw-r--r-- | src/Translate.ml | 18 | ||||
-rw-r--r-- | src/TranslateCore.ml | 2 | ||||
-rw-r--r-- | src/main.ml | 8 |
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 |