summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/InterpreterBorrows.ml3
-rw-r--r--src/Logging.ml3
-rw-r--r--src/PureMicroPasses.ml20
-rw-r--r--src/SymbolicToPure.ml9
-rw-r--r--src/Translate.ml42
-rw-r--r--src/TranslateCore.ml34
-rw-r--r--src/main.ml1
7 files changed, 70 insertions, 42 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index e7031d4c..f430c15d 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -11,6 +11,9 @@ open InterpreterUtils
open InterpreterBorrowsCore
open InterpreterProjectors
+(** The local logger *)
+let log = InterpreterBorrowsCore.log
+
(** Auxiliary function to end borrows: lookup a borrow in the environment,
update it (by returning an updated environment where the borrow has been
replaced by [Bottom])) if we can end the borrow (for instance, it is not
diff --git a/src/Logging.ml b/src/Logging.ml
index ad600adc..5605772d 100644
--- a/src/Logging.ml
+++ b/src/Logging.ml
@@ -15,6 +15,9 @@ let translate_log = L.get_logger "MainLogger.Translate"
(** Logger for SymbolicToPure *)
let symbolic_to_pure_log = L.get_logger "MainLogger.SymbolicToPure"
+(** Logger for PureMicroPasses *)
+let pure_micro_passes_log = L.get_logger "MainLogger.PureMicroPasses"
+
(** Logger for PureToExtract *)
let pure_to_extract_log = L.get_logger "MainLogger.PureToExtract"
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index aab19c11..3e04912a 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -2,6 +2,10 @@
open Errors
open Pure
+open TranslateCore
+
+(** The local logger *)
+let log = L.pure_micro_passes_log
type pn_ctx = string VarId.Map.t
(** "pretty-name context": see [compute_pretty_names] *)
@@ -297,3 +301,19 @@ let remove_meta (def : fun_def) : fun_def =
in
let body = obj#visit_expression () def.body in
{ def with body }
+
+(** Apply all the micro-passes to a function.
+
+ [ctx]: used only for printing.
+ *)
+let apply_passes_to_def (ctx : trans_ctx) (def : fun_def) : fun_def =
+ (* First, find names for the variables which are unnamed *)
+ let def = compute_pretty_names def in
+ log#ldebug (lazy ("compute_pretty_name:\n" ^ fun_def_to_string ctx def));
+
+ (* The meta-information is now useless: remove it *)
+ let def = remove_meta def in
+ log#ldebug (lazy ("remove_meta:\n" ^ fun_def_to_string ctx def));
+
+ (* We are done *)
+ def
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 8b31bffa..d46d8386 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1298,13 +1298,8 @@ let translate_fun_def (ctx : bs_ctx) (body : S.expression) : fun_def =
(* return *)
def
-let translate_type_defs (type_defs : T.type_def list) : type_def TypeDefId.Map.t
- =
- List.fold_left
- (fun tdefs def ->
- let tdef = translate_type_def def in
- TypeDefId.Map.add def.def_id tdef tdefs)
- TypeDefId.Map.empty type_defs
+let translate_type_defs (type_defs : T.type_def list) : type_def list =
+ List.map translate_type_def type_defs
(** Translates function signatures.
diff --git a/src/Translate.ml b/src/Translate.ml
index 1e8eb148..0971ba3d 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -6,31 +6,10 @@ module A = CfimAst
module M = Modules
module SA = SymbolicAst
module Micro = PureMicroPasses
+open TranslateCore
(** The local logger *)
-let log = L.translate_log
-
-type trans_ctx = { type_context : C.type_context; fun_context : C.fun_context }
-
-let type_def_to_string (ctx : trans_ctx) (def : Pure.type_def) : string =
- let type_params = def.type_params in
- let type_defs = ctx.type_context.type_defs in
- let fmt = PrintPure.mk_type_formatter type_defs type_params in
- PrintPure.type_def_to_string fmt def
-
-let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
- let type_params = sg.type_params in
- let type_defs = ctx.type_context.type_defs in
- let fun_defs = ctx.fun_context.fun_defs in
- let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
- PrintPure.fun_sig_to_string fmt sg
-
-let fun_def_to_string (ctx : trans_ctx) (def : Pure.fun_def) : string =
- let type_params = def.signature.type_params in
- let type_defs = ctx.type_context.type_defs in
- let fun_defs = ctx.fun_context.fun_defs in
- let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
- PrintPure.fun_def_to_string fmt def
+let log = TranslateCore.log
type symbolic_fun_translation = V.symbolic_value list * SA.expression
(** The result of running the symbolic interpreter on a function:
@@ -208,7 +187,7 @@ let translate_function_to_pure (config : C.partial_config)
(pure_forward, pure_backwards)
let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
- Pure.type_def T.TypeDefId.Map.t * pure_fun_translation A.FunDefId.Map.t =
+ Pure.type_def list * pure_fun_translation list =
(* Debug *)
log#ldebug (lazy "translate_module_to_pure");
@@ -243,19 +222,12 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
(* Translate all the functions *)
let pure_translations =
List.map
- (fun (fdef : A.fun_def) ->
- ( fdef.def_id,
- translate_function_to_pure config type_context fun_context fun_sigs
- fdef ))
+ (translate_function_to_pure config type_context fun_context fun_sigs)
m.functions
in
- (* Put the translated functions in a map *)
- let fun_defs =
- List.fold_left
- (fun m (def_id, trans) -> A.FunDefId.Map.add def_id trans m)
- A.FunDefId.Map.empty pure_translations
- in
+ (* (* Apply the micro-passes *)
+ let pure_translations = List.map (Micro.apply_passes_to_def ctx)*)
(* Return *)
- (type_defs, fun_defs)
+ (type_defs, pure_translations)
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
new file mode 100644
index 00000000..9374d3b9
--- /dev/null
+++ b/src/TranslateCore.ml
@@ -0,0 +1,34 @@
+(** Some utilities for the translation *)
+
+open InterpreterStatements
+open Interpreter
+module L = Logging
+module T = Types
+module A = CfimAst
+module M = Modules
+module SA = SymbolicAst
+
+(** The local logger *)
+let log = L.translate_log
+
+type trans_ctx = { type_context : C.type_context; fun_context : C.fun_context }
+
+let type_def_to_string (ctx : trans_ctx) (def : Pure.type_def) : string =
+ let type_params = def.type_params in
+ let type_defs = ctx.type_context.type_defs in
+ let fmt = PrintPure.mk_type_formatter type_defs type_params in
+ PrintPure.type_def_to_string fmt def
+
+let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
+ let type_params = sg.type_params in
+ let type_defs = ctx.type_context.type_defs in
+ let fun_defs = ctx.fun_context.fun_defs in
+ let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
+ PrintPure.fun_sig_to_string fmt sg
+
+let fun_def_to_string (ctx : trans_ctx) (def : Pure.fun_def) : string =
+ let type_params = def.signature.type_params in
+ let type_defs = ctx.type_context.type_defs in
+ let fun_defs = ctx.fun_context.fun_defs in
+ let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
+ PrintPure.fun_def_to_string fmt def
diff --git a/src/main.ml b/src/main.ml
index 1f996c2b..7381c648 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -55,6 +55,7 @@ let () =
borrows_log#set_level EL.Debug;
invariants_log#set_level EL.Warning;
symbolic_to_pure_log#set_level EL.Debug;
+ pure_micro_passes_log#set_level EL.Debug;
translate_log#set_level EL.Debug;
(* Load the module *)
let json = Yojson.Basic.from_file !filename in
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 05:45:57 +0000