diff options
| -rw-r--r-- | src/Interpreter.ml | 8 | ||||
| -rw-r--r-- | src/SymbolicAst.ml | 8 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 20 |
3 files changed, 25 insertions, 11 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index c7cdc329..bcfb9a78 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -43,7 +43,7 @@ let initialize_context (m : M.cfim_module) (type_vars : T.type_var list) : signature. *) let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) : - C.eval_ctx = + C.eval_ctx * 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 @@ -93,7 +93,7 @@ let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) : (* Push the remaining local variables (initialized with ⊥) *) let ctx = C.ctx_push_uninitialized_vars ctx local_vars in (* Return *) - ctx + (ctx, inst_sg) (** Small helper. @@ -184,7 +184,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ())); (* Create the evaluation context *) - let ctx = initialize_symbolic_context_for_fun m fdef in + let ctx, inst_sg = initialize_symbolic_context_for_fun m fdef in (* Create the continuation to finish the evaluation *) let config = C.config_of_partial C.SymbolicMode config in @@ -205,7 +205,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) let cf_move = move_return_value config in (* Generate the Return node *) let cf_return ret_value : m_fun = - fun _ -> Some (SA.Return ret_value) + fun _ -> Some (SA.Return (Some ret_value)) in (* Apply *) cf_move cf_return ctx diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml index 9dc20468..f0873aa3 100644 --- a/src/SymbolicAst.ml +++ b/src/SymbolicAst.ml @@ -28,9 +28,11 @@ type call = { used in CFIM: they are a first step towards lambda-calculus expressions. *) type expression = - | Return of V.typed_value - (** The typed value stored in [Return] is the value contained in the return - variable upon returning + | Return of V.typed_value option + (** There are two cases: + - the AST is for a forward function: the typed value should contain + the value which was in the return variable + - the AST is for a backward function: the typed value should be `None` *) | Panic | FunCall of call * expression diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 51d3c170..67d5cc45 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -190,7 +190,7 @@ type call_info = { type bs_ctx = { type_context : type_context; fun_context : fun_context; - bid : T.RegionGroupId.id option; + bid : T.RegionGroupId.id option; (** TODO: rename *) sv_to_var : var V.SymbolicValueId.Map.t; (** Whenever we encounter a new symbolic value (introduced because of a symbolic expansion or upon ending an abstraction, for instance) @@ -834,9 +834,7 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) : S.call * V.abs list = let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression = match e with - | S.Return v -> - let v = typed_value_to_rvalue ctx v in - Return v + | S.Return opt_v -> translate_return opt_v ctx | Panic -> Panic | FunCall (call, e) -> translate_function_call call e ctx | EndAbstraction (abs, e) -> translate_end_abstraction abs e ctx @@ -845,6 +843,20 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression = (* We ignore the meta information *) translate_expression e ctx +and translate_return (opt_v : V.typed_value option) (ctx : bs_ctx) : expression + = + (* There are two cases: + - either we are translating a forward function, in which case the optional + value should be `Some` (it is the returned value) + - or we are translating a backward function, in which case it should be `None` + *) + match ctx.bid with + | None -> + let v = Option.get opt_v in + let v = typed_value_to_rvalue ctx v in + Return v + | Some bid -> raise Unimplemented + and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : expression = (* Translate the function call *) |