From ba61ed50e7b2fdc78690de92d734a3747029f903 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Wed, 8 Jun 2022 12:32:14 +0200 Subject: read globals from LLBC JSON into functions --- src/TranslateCore.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'src/TranslateCore.ml') diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index 17c35cbf..3d3887ce 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -1,6 +1,7 @@ (** Some utilities for the translation *) open InterpreterStatements +open FunIdentifier module L = Logging module T = Types module A = LlbcAst @@ -14,8 +15,8 @@ let log = L.translate_log type type_context = C.type_context [@@deriving show] type fun_context = { - fun_decls : A.fun_decl A.FunDeclId.Map.t; - fun_infos : FA.fun_info A.FunDeclId.Map.t; + fun_decls : A.fun_decl FunDeclId.Map.t; + fun_infos : FA.fun_info FunDeclId.Map.t; } [@@deriving show] @@ -49,6 +50,6 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in PrintPure.fun_decl_to_string fmt def -let fun_decl_id_to_string (ctx : trans_ctx) (id : Pure.FunDeclId.id) : string = +let fun_decl_id_to_string (ctx : trans_ctx) (id : FunDeclId.id) : string = Print.fun_name_to_string - (Pure.FunDeclId.Map.find id ctx.fun_context.fun_decls).name + (FunDeclId.Map.find id ctx.fun_context.fun_decls).name -- cgit v1.2.3 From 7703c4ca86a390303d0a120f8811c8fd704c5168 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Tue, 21 Jun 2022 11:41:09 +0200 Subject: concrete & symbolic evaluation work with new LLBC format --- src/TranslateCore.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src/TranslateCore.ml') diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index 3d3887ce..ccaa9e22 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -1,7 +1,6 @@ (** Some utilities for the translation *) open InterpreterStatements -open FunIdentifier module L = Logging module T = Types module A = LlbcAst @@ -15,8 +14,9 @@ let log = L.translate_log type type_context = C.type_context [@@deriving show] type fun_context = { - fun_decls : A.fun_decl FunDeclId.Map.t; - fun_infos : FA.fun_info FunDeclId.Map.t; + fun_decls : A.fun_decl A.FunDeclId.Map.t; + fun_infos : FA.fun_info A.FunDeclId.Map.t; + gid_conv : A.global_id_converter; } [@@deriving show] @@ -50,6 +50,6 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in PrintPure.fun_decl_to_string fmt def -let fun_decl_id_to_string (ctx : trans_ctx) (id : FunDeclId.id) : string = +let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string = Print.fun_name_to_string - (FunDeclId.Map.find id ctx.fun_context.fun_decls).name + (A.FunDeclId.Map.find id ctx.fun_context.fun_decls).name -- cgit v1.2.3 From 47691de8fe3dc32a29663d4d8343eb415ce1d81e Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Thu, 30 Jun 2022 12:22:14 +0200 Subject: Traduct globals body separately (WIP) --- src/TranslateCore.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/TranslateCore.ml') diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index ccaa9e22..047219ad 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -40,14 +40,16 @@ let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string = let type_params = sg.type_params in let type_decls = ctx.type_context.type_decls in let fun_decls = ctx.fun_context.fun_decls in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in + let gid_conv = ctx.fun_context.gid_conv in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in PrintPure.fun_sig_to_string fmt sg let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = let type_params = def.signature.type_params in let type_decls = ctx.type_context.type_decls in let fun_decls = ctx.fun_context.fun_decls in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in + let gid_conv = ctx.fun_context.gid_conv in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in PrintPure.fun_decl_to_string fmt def let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string = -- cgit v1.2.3 From f9b324be57708e9496ca6e9ac0b7e68ffd9e7108 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Mon, 18 Jul 2022 16:27:00 +0200 Subject: Address much stuff of the PR, throw exceptions at remaining places --- src/TranslateCore.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'src/TranslateCore.ml') diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index 047219ad..e77445cd 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -16,11 +16,16 @@ type type_context = C.type_context [@@deriving show] type fun_context = { fun_decls : A.fun_decl A.FunDeclId.Map.t; fun_infos : FA.fun_info A.FunDeclId.Map.t; - gid_conv : A.global_id_converter; } [@@deriving show] -type trans_ctx = { type_context : type_context; fun_context : fun_context } +type global_context = C.global_context [@@deriving show] + +type trans_ctx = { + type_context : type_context; + fun_context : fun_context; + global_context : global_context +} type pure_fun_translation = Pure.fun_decl * Pure.fun_decl list @@ -40,16 +45,16 @@ let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string = let type_params = sg.type_params in let type_decls = ctx.type_context.type_decls in let fun_decls = ctx.fun_context.fun_decls in - let gid_conv = ctx.fun_context.gid_conv in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in + let global_decls = ctx.global_context.global_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in PrintPure.fun_sig_to_string fmt sg let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = let type_params = def.signature.type_params in let type_decls = ctx.type_context.type_decls in let fun_decls = ctx.fun_context.fun_decls in - let gid_conv = ctx.fun_context.gid_conv in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in + let global_decls = ctx.global_context.global_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in PrintPure.fun_decl_to_string fmt def let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string = -- cgit v1.2.3 From 4a8b4b1be044ffaa8de72cf847c00184b6b8ab40 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 22 Sep 2022 18:45:25 +0200 Subject: Reformat the project with dune --- src/TranslateCore.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'src/TranslateCore.ml') diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index e77445cd..326bb05f 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -24,7 +24,7 @@ type global_context = C.global_context [@@deriving show] type trans_ctx = { type_context : type_context; fun_context : fun_context; - global_context : global_context + global_context : global_context; } type pure_fun_translation = Pure.fun_decl * Pure.fun_decl list @@ -46,7 +46,9 @@ let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string = let type_decls = ctx.type_context.type_decls in let fun_decls = ctx.fun_context.fun_decls in let global_decls = ctx.global_context.global_decls in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in + let fmt = + PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params + in PrintPure.fun_sig_to_string fmt sg let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = @@ -54,7 +56,9 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = let type_decls = ctx.type_context.type_decls in let fun_decls = ctx.fun_context.fun_decls in let global_decls = ctx.global_context.global_decls in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in + let fmt = + PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params + in PrintPure.fun_decl_to_string fmt def let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string = -- cgit v1.2.3