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/Interpreter.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/Interpreter.ml') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index f6ae268d..702aeea6 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1,4 +1,5 @@ open Cps +open FunIdentifier open InterpreterUtils open InterpreterProjectors open InterpreterBorrows @@ -255,9 +256,9 @@ module Test = struct environment. *) let test_unit_function (config : C.partial_config) (m : M.llbc_module) - (fid : A.FunDeclId.id) : unit = + (fid : FunDeclId.id) : unit = (* Retrieve the function declaration *) - let fdef = A.FunDeclId.nth m.functions fid in + let fdef = FunDeclId.nth m.functions fid in let body = Option.get fdef.body in (* Debug *) -- 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/Interpreter.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'src/Interpreter.ml') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 702aeea6..5affea4c 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1,5 +1,4 @@ open Cps -open FunIdentifier open InterpreterUtils open InterpreterProjectors open InterpreterBorrows @@ -25,7 +24,7 @@ let compute_type_fun_contexts (m : M.llbc_module) : TypesAnalysis.analyze_type_declarations type_decls type_decls_list in let type_context = { C.type_decls_groups; type_decls; type_infos } in - let fun_context = { C.fun_decls } in + let fun_context = { C.fun_decls; gid_conv = m.gid_conv } in (type_context, fun_context) let initialize_eval_context (type_context : C.type_context) @@ -256,9 +255,9 @@ module Test = struct environment. *) let test_unit_function (config : C.partial_config) (m : M.llbc_module) - (fid : FunDeclId.id) : unit = + (fid : A.FunDeclId.id) : unit = (* Retrieve the function declaration *) - let fdef = FunDeclId.nth m.functions fid in + let fdef = A.FunDeclId.nth m.functions fid in let body = Option.get fdef.body in (* Debug *) -- 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/Interpreter.ml | 44 ++++++++++++++++++++++++++------------------ 1 file changed, 26 insertions(+), 18 deletions(-) (limited to 'src/Interpreter.ml') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index f4f01ff8..3610d486 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -14,9 +14,9 @@ module SA = SymbolicAst let log = L.interpreter_log let compute_type_fun_contexts (m : M.llbc_module) : - C.type_context * C.fun_context = + C.type_context * C.fun_context * C.global_context = let type_decls_list, _ = M.split_declarations m.declarations in - let type_decls, fun_decls = M.compute_defs_maps m in + let type_decls, fun_decls, global_decls = M.compute_defs_maps m in let type_decls_groups, _funs_defs_groups = M.split_declarations_to_group_maps m.declarations in @@ -24,15 +24,20 @@ let compute_type_fun_contexts (m : M.llbc_module) : TypesAnalysis.analyze_type_declarations type_decls type_decls_list in let type_context = { C.type_decls_groups; type_decls; type_infos } in - let fun_context = { C.fun_decls; gid_conv = m.gid_conv } in - (type_context, fun_context) - -let initialize_eval_context (type_context : C.type_context) - (fun_context : C.fun_context) (type_vars : T.type_var list) : C.eval_ctx = + let fun_context = { C.fun_decls } in + let global_context = { C.global_decls } in + (type_context, fun_context, global_context) + +let initialize_eval_context + (type_context : C.type_context) + (fun_context : C.fun_context) + (global_context : C.global_context) + (type_vars : T.type_var list) : C.eval_ctx = C.reset_global_counters (); { C.type_context; C.fun_context; + C.global_context; C.type_vars; C.env = [ C.Frame ]; C.ended_regions = T.RegionId.Set.empty; @@ -51,8 +56,11 @@ let initialize_eval_context (type_context : C.type_context) - the list of symbolic values introduced for the input values - the instantiated function signature *) -let initialize_symbolic_context_for_fun (type_context : C.type_context) - (fun_context : C.fun_context) (fdef : A.fun_decl) : +let initialize_symbolic_context_for_fun + (type_context : C.type_context) + (fun_context : C.fun_context) + (global_context : C.global_context) + (fdef : A.fun_decl) : C.eval_ctx * V.symbolic_value list * A.inst_fun_sig = (* The abstractions are not initialized the same way as for function * calls: they contain *loan* projectors, because they "provide" us @@ -67,7 +75,7 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context) * *) let sg = fdef.signature in (* Create the context *) - let ctx = initialize_eval_context type_context fun_context sg.type_params in + let ctx = initialize_eval_context type_context fun_context global_context sg.type_params in (* Instantiate the signature *) let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in let inst_sg = instantiate_fun_sig type_params sg in @@ -204,7 +212,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return - the symbolic AST generated by the symbolic execution *) let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) - (type_context : C.type_context) (fun_context : C.fun_context) + (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context) (fdef : A.fun_decl) (back_id : T.RegionGroupId.id option) : V.symbolic_value list * SA.expression option = (* Debug *) @@ -218,7 +226,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) (* Create the evaluation context *) let ctx, input_svs, inst_sg = - initialize_symbolic_context_for_fun type_context fun_context fdef + initialize_symbolic_context_for_fun type_context fun_context global_context fdef in (* Create the continuation to finish the evaluation *) @@ -285,8 +293,8 @@ module Test = struct assert (body.A.arg_count = 0); (* Create the evaluation context *) - let type_context, fun_context = compute_type_fun_contexts m in - let ctx = initialize_eval_context type_context fun_context [] in + let type_context, fun_context, global_context = compute_type_fun_contexts m in + let ctx = initialize_eval_context type_context fun_context global_context [] in (* Insert the (uninitialized) local variables *) let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in @@ -330,7 +338,7 @@ module Test = struct (** Execute the symbolic interpreter on a function. *) let test_function_symbolic (config : C.partial_config) (synthesize : bool) - (type_context : C.type_context) (fun_context : C.fun_context) + (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context) (fdef : A.fun_decl) : unit = (* Debug *) log#ldebug @@ -338,7 +346,7 @@ module Test = struct (* Evaluate *) let evaluate = - evaluate_function_symbolic config synthesize type_context fun_context fdef + evaluate_function_symbolic config synthesize type_context fun_context global_context fdef in (* Execute the forward function *) let _ = evaluate None in @@ -368,12 +376,12 @@ module Test = struct in (* Filter the opaque functions *) let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in - let type_context, fun_context = compute_type_fun_contexts m in + let type_context, fun_context, global_context = compute_type_fun_contexts m in let test_fun (def : A.fun_decl) : unit = (* Execute the function - note that as the symbolic interpreter explores * all the path, some executions are expected to "panic": we thus don't * check the return value *) - test_function_symbolic config synthesize type_context fun_context def + test_function_symbolic config synthesize type_context fun_context global_context def in List.iter test_fun no_loop_funs end -- cgit v1.2.3 From f9015d1e956ace6c875eb6a631caeac49cfb8148 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Fri, 29 Jul 2022 16:04:49 +0200 Subject: Create global declaration group, address PR changes but introduce bugs --- src/Interpreter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Interpreter.ml') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 3610d486..51144ba2 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -15,9 +15,9 @@ let log = L.interpreter_log let compute_type_fun_contexts (m : M.llbc_module) : C.type_context * C.fun_context * C.global_context = - let type_decls_list, _ = M.split_declarations m.declarations in + let type_decls_list, _, _ = M.split_declarations m.declarations in let type_decls, fun_decls, global_decls = M.compute_defs_maps m in - let type_decls_groups, _funs_defs_groups = + let type_decls_groups, _funs_defs_groups, _globals_defs_groups = M.split_declarations_to_group_maps m.declarations in let type_infos = -- cgit v1.2.3 From c8ccd864e1fa6de3241d9dba184cf8ee4101e421 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 22 Sep 2022 17:52:27 +0200 Subject: Make minor cleanup --- src/Interpreter.ml | 52 ++++++++++++++++++++++++++++++---------------------- 1 file changed, 30 insertions(+), 22 deletions(-) (limited to 'src/Interpreter.ml') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 51144ba2..3a2939ef 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -13,7 +13,7 @@ module SA = SymbolicAst (** The local logger *) let log = L.interpreter_log -let compute_type_fun_contexts (m : M.llbc_module) : +let compute_type_fun_global_contexts (m : M.llbc_module) : C.type_context * C.fun_context * C.global_context = let type_decls_list, _, _ = M.split_declarations m.declarations in let type_decls, fun_decls, global_decls = M.compute_defs_maps m in @@ -28,10 +28,8 @@ let compute_type_fun_contexts (m : M.llbc_module) : let global_context = { C.global_decls } in (type_context, fun_context, global_context) -let initialize_eval_context - (type_context : C.type_context) - (fun_context : C.fun_context) - (global_context : C.global_context) +let initialize_eval_context (type_context : C.type_context) + (fun_context : C.fun_context) (global_context : C.global_context) (type_vars : T.type_var list) : C.eval_ctx = C.reset_global_counters (); { @@ -56,12 +54,9 @@ let initialize_eval_context - the list of symbolic values introduced for the input values - the instantiated function signature *) -let initialize_symbolic_context_for_fun - (type_context : C.type_context) - (fun_context : C.fun_context) - (global_context : C.global_context) - (fdef : A.fun_decl) : - C.eval_ctx * V.symbolic_value list * A.inst_fun_sig = +let initialize_symbolic_context_for_fun (type_context : C.type_context) + (fun_context : C.fun_context) (global_context : C.global_context) + (fdef : A.fun_decl) : C.eval_ctx * V.symbolic_value list * A.inst_fun_sig = (* The abstractions are not initialized the same way as for function * calls: they contain *loan* projectors, because they "provide" us * with the input values (which behave as if they had been returned @@ -75,7 +70,10 @@ let initialize_symbolic_context_for_fun * *) let sg = fdef.signature in (* Create the context *) - let ctx = initialize_eval_context type_context fun_context global_context sg.type_params in + let ctx = + initialize_eval_context type_context fun_context global_context + sg.type_params + in (* Instantiate the signature *) let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in let inst_sg = instantiate_fun_sig type_params sg in @@ -212,8 +210,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return - the symbolic AST generated by the symbolic execution *) let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) - (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context) - (fdef : A.fun_decl) (back_id : T.RegionGroupId.id option) : + (type_context : C.type_context) (fun_context : C.fun_context) + (global_context : C.global_context) (fdef : A.fun_decl) + (back_id : T.RegionGroupId.id option) : V.symbolic_value list * SA.expression option = (* Debug *) let name_to_string () = @@ -226,7 +225,8 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) (* Create the evaluation context *) let ctx, input_svs, inst_sg = - initialize_symbolic_context_for_fun type_context fun_context global_context fdef + initialize_symbolic_context_for_fun type_context fun_context global_context + fdef in (* Create the continuation to finish the evaluation *) @@ -293,8 +293,12 @@ module Test = struct assert (body.A.arg_count = 0); (* Create the evaluation context *) - let type_context, fun_context, global_context = compute_type_fun_contexts m in - let ctx = initialize_eval_context type_context fun_context global_context [] in + let type_context, fun_context, global_context = + compute_type_fun_global_contexts m + in + let ctx = + initialize_eval_context type_context fun_context global_context [] + in (* Insert the (uninitialized) local variables *) let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in @@ -338,15 +342,16 @@ module Test = struct (** Execute the symbolic interpreter on a function. *) let test_function_symbolic (config : C.partial_config) (synthesize : bool) - (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context) - (fdef : A.fun_decl) : unit = + (type_context : C.type_context) (fun_context : C.fun_context) + (global_context : C.global_context) (fdef : A.fun_decl) : unit = (* Debug *) log#ldebug (lazy ("test_function_symbolic: " ^ Print.fun_name_to_string fdef.A.name)); (* Evaluate *) let evaluate = - evaluate_function_symbolic config synthesize type_context fun_context global_context fdef + evaluate_function_symbolic config synthesize type_context fun_context + global_context fdef in (* Execute the forward function *) let _ = evaluate None in @@ -376,12 +381,15 @@ module Test = struct in (* Filter the opaque functions *) let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in - let type_context, fun_context, global_context = compute_type_fun_contexts m in + let type_context, fun_context, global_context = + compute_type_fun_global_contexts m + in let test_fun (def : A.fun_decl) : unit = (* Execute the function - note that as the symbolic interpreter explores * all the path, some executions are expected to "panic": we thus don't * check the return value *) - test_function_symbolic config synthesize type_context fun_context global_context def + test_function_symbolic config synthesize type_context fun_context + global_context def in List.iter test_fun no_loop_funs end -- cgit v1.2.3