diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 26 | ||||
| -rw-r--r-- | src/Translate.ml | 39 |
2 files changed, 49 insertions, 16 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 diff --git a/src/Translate.ml b/src/Translate.ml index ecc97ed1..ec580258 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -9,6 +9,12 @@ module SA = SymbolicAst (** The local logger *) let log = L.translate_log +type symbolic_fun_translation = V.symbolic_value list * SA.expression +(** The result of running the symbolic interpreter on a function: + - the list of symbolic values used for the input values + - the generated symbolic AST + *) + type pure_fun_translation = Pure.fun_def * Pure.fun_def list (** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs, @@ -16,7 +22,8 @@ type pure_fun_translation = Pure.fun_def * Pure.fun_def list *) let translate_function_to_symbolics (config : C.partial_config) (type_context : C.type_context) (fun_context : C.fun_context) - (fdef : A.fun_def) : SA.expression * SA.expression list = + (fdef : A.fun_def) : + symbolic_fun_translation * symbolic_fun_translation list = (* Debug *) log#ldebug (lazy @@ -24,15 +31,19 @@ let translate_function_to_symbolics (config : C.partial_config) (* Evaluate *) let synthesize = true in - let evaluate = - evaluate_function_symbolic config synthesize type_context fun_context fdef + let evaluate gid = + let inputs, symb = + evaluate_function_symbolic config synthesize type_context fun_context fdef + gid + in + (inputs, Option.get symb) in (* Execute the forward function *) - let forward = Option.get (evaluate None) in + let forward = evaluate None in (* Execute the backward functions *) let backwards = T.RegionGroupId.mapi - (fun gid _ -> Option.get (evaluate (Some gid))) + (fun gid _ -> evaluate (Some gid)) fdef.signature.regions_hierarchy in @@ -90,17 +101,24 @@ let translate_function_to_pure (config : C.partial_config) } in - (* We need to initialize the input/output variables. First, the inputs - * for the forward function *) + (* We need to initialize the input/output variables *) let module RegularFunIdMap = SymbolicToPure.RegularFunIdMap in let forward_sg = RegularFunIdMap.find (A.Local def_id, None) fun_sigs in + let add_forward_inputs input_svs ctx = + let ctx, forward_inputs = + SymbolicToPure.fresh_vars_for_symbolic_values input_svs ctx + in + { ctx with forward_inputs } + in let ctx, forward_inputs = SymbolicToPure.fresh_vars forward_sg.inputs ctx in let ctx = { ctx with forward_inputs } in (* Translate the forward function *) let pure_forward = - SymbolicToPure.translate_fun_def fdef ctx symbolic_forward + SymbolicToPure.translate_fun_def fdef + (add_forward_inputs (fst symbolic_forward) ctx) + (snd symbolic_forward) in (* Translate the backward functions *) @@ -109,8 +127,10 @@ let translate_function_to_pure (config : C.partial_config) * there are no nested borrows for now, and so that the region groups * can't have parents *) assert (rg.parents = []); - (* TODO: the computation of the backward inputs is a bit awckward... *) let back_id = rg.id in + let input_svs, symbolic = T.RegionGroupId.nth symbolic_backwards back_id in + let ctx = add_forward_inputs input_svs ctx in + (* TODO: the computation of the backward inputs is a bit awckward... *) let backward_sg = RegularFunIdMap.find (A.Local def_id, Some back_id) fun_sigs in @@ -135,7 +155,6 @@ let translate_function_to_pure (config : C.partial_config) in (* Translate *) - let symbolic = T.RegionGroupId.nth symbolic_backwards back_id in SymbolicToPure.translate_fun_def fdef ctx symbolic in let pure_backwards = |