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/InterpreterStatements.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/InterpreterStatements.ml') diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 1083d643..c7308720 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -7,6 +7,7 @@ module A = LlbcAst module L = Logging open TypesUtils open ValuesUtils +open FunIdentifier module Inv = Invariants module S = SynthesizeSymbolic open Errors @@ -1001,7 +1002,7 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = call.args call.dest (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) -and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) +and eval_local_function_call_concrete (config : C.config) (fid : FunDeclId.id) (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> @@ -1079,7 +1080,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) cc cf ctx (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) -and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) +and eval_local_function_call_symbolic (config : C.config) (fid : FunDeclId.id) (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> @@ -1300,7 +1301,7 @@ and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id) (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for [eval_statement]) *) -and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id) +and eval_local_function_call (config : C.config) (fid : FunDeclId.id) (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = match config.mode with -- 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/InterpreterStatements.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'src/InterpreterStatements.ml') diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index c7308720..e5564d59 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -7,7 +7,6 @@ module A = LlbcAst module L = Logging open TypesUtils open ValuesUtils -open FunIdentifier module Inv = Invariants module S = SynthesizeSymbolic open Errors @@ -822,6 +821,15 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cf_eval_rvalue cf_assign cf ctx + | A.AssignGlobal { dst; global } -> + let call : A.call = { + func = A.Regular (A.global_to_fun_id ctx.fun_context.gid_conv global); + region_args = []; + type_args = []; + args = []; + dest = { var_id = dst; projection = [] }; + } in + eval_function_call config call cf ctx | A.FakeRead p -> let expand_prim_copy = false in let cf_prepare = prepare_rplace config expand_prim_copy Read p in @@ -1002,7 +1010,7 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = call.args call.dest (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) -and eval_local_function_call_concrete (config : C.config) (fid : FunDeclId.id) +and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> @@ -1080,7 +1088,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : FunDeclId.id) cc cf ctx (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) -and eval_local_function_call_symbolic (config : C.config) (fid : FunDeclId.id) +and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> @@ -1301,7 +1309,7 @@ and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id) (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for [eval_statement]) *) -and eval_local_function_call (config : C.config) (fid : FunDeclId.id) +and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id) (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = match config.mode with -- 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/InterpreterStatements.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/InterpreterStatements.ml') diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 8f981174..6a0b81f3 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -832,8 +832,9 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cf_eval_rvalue cf_assign cf ctx | A.AssignGlobal { dst; global } -> + (* What codegen do we want ? *) let call : A.call = { - func = A.Regular (A.global_to_fun_id ctx.fun_context.gid_conv global); + func = A.Regular (failwith "TODO InterpretStatements.ml:837"); region_args = []; type_args = []; args = []; -- cgit v1.2.3 From af298b98b7efe8c6dba86a99dc9c07c3c43ce14d Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Thu, 28 Jul 2022 14:24:41 +0200 Subject: Always put can_fail to true, specialize global traduction to concrete function call and symbolic fresh value --- src/InterpreterStatements.ml | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) (limited to 'src/InterpreterStatements.ml') diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 6a0b81f3..3f6470b9 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -832,15 +832,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cf_eval_rvalue cf_assign cf ctx | A.AssignGlobal { dst; global } -> - (* What codegen do we want ? *) - let call : A.call = { - func = A.Regular (failwith "TODO InterpretStatements.ml:837"); - region_args = []; - type_args = []; - args = []; - dest = { var_id = dst; projection = [] }; - } in - eval_function_call config call cf ctx + eval_global config dst global cf ctx | A.FakeRead p -> let expand_prim_copy = false in let cf_prepare cf = @@ -918,6 +910,21 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cc cf_eval_st cf ctx +and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.id) : st_cm_fun = + fun cf ctx -> + let global = C.ctx_lookup_global_decl ctx gid in + let place = { E.var_id = dest; projection = [] } in + match config.mode with + | ConcreteMode -> + (* Treat the global as a function without arguments to call *) + (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx + | SymbolicMode -> + (* Treat the global as a fresh symbolic value *) + let rty = ety_no_regions_to_rty global.ty in + let sval = mk_fresh_symbolic_value V.FunCallRet rty in + let sval = mk_typed_value_from_symbolic_value sval in + assign_to_place config sval place (cf Unit) ctx + (** Evaluate a switch *) and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : st_cm_fun = -- 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/InterpreterStatements.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'src/InterpreterStatements.ml') diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 3f6470b9..ffc47741 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -919,11 +919,16 @@ and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.i (* Treat the global as a function without arguments to call *) (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx | SymbolicMode -> + (* + let g = A.GlobalDeclId.Map.find gid ctx.global_context.global_decls in + (eval_local_function_call_symbolic config g.body_id [] [] [] place) cf ctx + *) + failwith "TODO Got error later in translate_fun_decl>meta>expansion ~> lookup_var_for_symbolic_value"; (* Treat the global as a fresh symbolic value *) let rty = ety_no_regions_to_rty global.ty in let sval = mk_fresh_symbolic_value V.FunCallRet rty in let sval = mk_typed_value_from_symbolic_value sval in - assign_to_place config sval place (cf Unit) ctx + (assign_to_place config sval place) (cf Unit) ctx (** Evaluate a switch *) and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : -- cgit v1.2.3 From 3c5fb260012ee8bb8b9fd90bc4624d893ac7678a Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Mon, 8 Aug 2022 15:16:14 +0200 Subject: Register global names, one error remaining --- src/InterpreterStatements.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'src/InterpreterStatements.ml') diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index ffc47741..31c3aabb 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -919,16 +919,20 @@ and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.i (* Treat the global as a function without arguments to call *) (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx | SymbolicMode -> + (* Treat the global as a fresh symbolic value *) + (* let g = A.GlobalDeclId.Map.find gid ctx.global_context.global_decls in (eval_local_function_call_symbolic config g.body_id [] [] [] place) cf ctx - *) + failwith "TODO Got error later in translate_fun_decl>meta>expansion ~> lookup_var_for_symbolic_value"; - (* Treat the global as a fresh symbolic value *) + *) + let rty = ety_no_regions_to_rty global.ty in let sval = mk_fresh_symbolic_value V.FunCallRet rty in let sval = mk_typed_value_from_symbolic_value sval in (assign_to_place config sval place) (cf Unit) ctx + (** Evaluate a switch *) and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : -- cgit v1.2.3 From cd754eabe3af025ca3465c5fc6d8cb48da66a1ae Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Wed, 10 Aug 2022 18:56:25 +0200 Subject: Corrected translation without using functions, remaining bug in hashmap translation --- src/InterpreterStatements.ml | 17 ++++------------- 1 file changed, 4 insertions(+), 13 deletions(-) (limited to 'src/InterpreterStatements.ml') diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 31c3aabb..48620439 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -920,19 +920,10 @@ and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.i (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx | SymbolicMode -> (* Treat the global as a fresh symbolic value *) - - (* - let g = A.GlobalDeclId.Map.find gid ctx.global_context.global_decls in - (eval_local_function_call_symbolic config g.body_id [] [] [] place) cf ctx - - failwith "TODO Got error later in translate_fun_decl>meta>expansion ~> lookup_var_for_symbolic_value"; - *) - - let rty = ety_no_regions_to_rty global.ty in - let sval = mk_fresh_symbolic_value V.FunCallRet rty in - let sval = mk_typed_value_from_symbolic_value sval in - (assign_to_place config sval place) (cf Unit) ctx - + let sval = mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty) in + let cc = assign_to_place config (mk_typed_value_from_symbolic_value sval) place in + let e = cc (cf Unit) ctx in + S.synthesize_global_eval gid sval e (** Evaluate a switch *) and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : -- cgit v1.2.3 From f106fd4ad0a221611c840bf0af0b1c2ff23f3d0f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 22 Sep 2022 17:44:04 +0200 Subject: Make minor modifications --- src/InterpreterStatements.ml | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) (limited to 'src/InterpreterStatements.ml') diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 48620439..34310ea1 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -831,8 +831,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cf_eval_rvalue cf_assign cf ctx - | A.AssignGlobal { dst; global } -> - eval_global config dst global cf ctx + | A.AssignGlobal { dst; global } -> eval_global config dst global cf ctx | A.FakeRead p -> let expand_prim_copy = false in let cf_prepare cf = @@ -910,20 +909,27 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cc cf_eval_st cf ctx -and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.id) : st_cm_fun = +and eval_global (config : C.config) (dest : V.VarId.id) + (gid : LA.GlobalDeclId.id) : st_cm_fun = fun cf ctx -> let global = C.ctx_lookup_global_decl ctx gid in let place = { E.var_id = dest; projection = [] } in match config.mode with | ConcreteMode -> - (* Treat the global as a function without arguments to call *) - (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx + (* Treat the evaluation of the global as a call to the global body (without arguments) *) + (eval_local_function_call_concrete config global.body_id [] [] [] place) + cf ctx | SymbolicMode -> - (* Treat the global as a fresh symbolic value *) - let sval = mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty) in - let cc = assign_to_place config (mk_typed_value_from_symbolic_value sval) place in - let e = cc (cf Unit) ctx in - S.synthesize_global_eval gid sval e + (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be + * defined as equal to the value of the global (see `S.synthesize_global_eval`). *) + let sval = + mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty) + in + let cc = + assign_to_place config (mk_typed_value_from_symbolic_value sval) place + in + let e = cc (cf Unit) ctx in + S.synthesize_global_eval gid sval e (** Evaluate a switch *) and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : -- cgit v1.2.3