diff options
Diffstat (limited to 'src/Interpreter.ml')
| -rw-r--r-- | src/Interpreter.ml | 26 |
1 files changed, 20 insertions, 6 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 24d71234..b1f889cb 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -45,10 +45,15 @@ let initialize_eval_context (type_context : C.type_context) - the remaining locals are initialized as ⊥ Abstractions are introduced for the regions present in the function signature. + + We return: + - the initialized evaluation 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_def) : - C.eval_ctx * A.inst_fun_sig = + 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 @@ -98,7 +103,7 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context) (* Push the remaining local variables (initialized with ⊥) *) let ctx = C.ctx_push_uninitialized_vars ctx local_vars in (* Return *) - (ctx, inst_sg) + (ctx, input_svs, inst_sg) (** Small helper. @@ -171,11 +176,17 @@ let evaluate_function_symbolic_synthesize_backward_from_return in cf_move_ret cf_consume_ret ctx -(** Evaluate a function with the symbolic interpreter *) +(** Evaluate a function with the symbolic interpreter. + + We return: + - the list of symbolic values introduced for the input values (this is useful + for the synthesis) + - 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) (fdef : A.fun_def) (back_id : T.RegionGroupId.id option) : - SA.expression option = + V.symbolic_value list * SA.expression option = (* Debug *) let name_to_string () = Print.name_to_string fdef.A.name @@ -186,7 +197,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, inst_sg = + let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun type_context fun_context fdef in @@ -227,7 +238,10 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) in (* Evaluate the function *) - eval_function_body config fdef.A.body cf_finish ctx + let symbolic = eval_function_body config fdef.A.body cf_finish ctx in + + (* Return *) + (input_svs, symbolic) module Test = struct (** Test a unit function (taking no arguments) by evaluating it in an empty |