Rename CFIM to LLBC

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