diff options
| -rw-r--r-- | src/Interpreter.ml | 47 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 19 | ||||
| -rw-r--r-- | src/Synthesis.ml | 6 |
3 files changed, 49 insertions, 23 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index ec1e6373..dcdf6026 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -2,8 +2,8 @@ module L = Logging module T = Types module A = CfimAst module M = Modules +open Cps open InterpreterUtils -open InterpreterExpressions open InterpreterStatements (* TODO: it would be good to find a "core", which implements the rules (like @@ -116,7 +116,7 @@ module Test = struct environment. *) let test_unit_function (config : C.partial_config) (m : M.cfim_module) - (fid : A.FunDefId.id) : unit eval_result = + (fid : A.FunDefId.id) : unit = (* Retrieve the function declaration *) let fdef = A.FunDefId.nth m.functions fid in @@ -135,14 +135,20 @@ module Test = struct (* Insert the (uninitialized) local variables *) let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in + (* Create the continuation to check the function's result *) + let cf_check res _ = + match res with + | Return -> (* Ok *) None + | _ -> + failwith + ("Unit test failed (concrete execution) on: " + ^ Print.name_to_string fdef.A.name) + in + (* Evaluate the function *) let config = C.config_of_partial C.ConcreteMode config in - match eval_function_body config ctx fdef.A.body with - | [ Ok _ ] -> Ok () - | [ Error err ] -> Error err - | _ -> - (* We execute the concrete interpreter: there shouldn't be any branching *) - failwith "Unreachable" + let _ = eval_function_body config fdef.A.body cf_check ctx in + () (** Small helper: return true if the function is a unit function (no parameters, no arguments) - TODO: move *) @@ -157,15 +163,13 @@ module Test = struct = let unit_funs = List.filter fun_def_is_unit m.functions in let test_unit_fun (def : A.fun_def) : unit = - match test_unit_function config m def.A.def_id with - | Error _ -> failwith "Unit test failed (concrete execution)" - | Ok _ -> () + test_unit_function config m def.A.def_id in List.iter test_unit_fun unit_funs (** Execute the symbolic interpreter on a function. *) let test_function_symbolic (config : C.partial_config) (m : M.cfim_module) - (fid : A.FunDefId.id) : C.eval_ctx eval_result list = + (fid : A.FunDefId.id) : unit = (* Retrieve the function declaration *) let fdef = A.FunDefId.nth m.functions fid in @@ -176,9 +180,23 @@ module Test = struct (* Create the evaluation context *) let ctx = initialize_symbolic_context_for_fun m fdef in + (* Create the continuation to check the function's result *) + let cf_check res _ = + match res with + | Return | Panic -> + (* Note that as we explore all the execution branches, one of + * the executions can lead to a panic *) + None + | _ -> + failwith + ("Unit test failed (symbolic execution) on: " + ^ Print.name_to_string fdef.A.name) + in + (* Evaluate the function *) let config = C.config_of_partial C.SymbolicMode config in - eval_function_body config ctx fdef.A.body + let _ = eval_function_body config fdef.A.body cf_check ctx in + () (** Execute the symbolic interpreter on a list of functions. @@ -194,8 +212,7 @@ module Test = struct (* 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 *) - let _ = test_function_symbolic config m def.A.def_id in - () + test_function_symbolic config m def.A.def_id in List.iter test_fun no_loop_funs end diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index bf02cbd6..1a6e198c 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -421,6 +421,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config) (sv : V.symbolic_value) (see_cf_l : (symbolic_expansion option * m_fun) list) : m_fun = fun ctx -> + assert (see_cf_l <> []); (* Apply the symbolic expansion in in the context and call the continuation *) let resl = List.map @@ -432,13 +433,21 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config) | Some see -> apply_symbolic_expansion_non_borrow config sv see ctx in (* Continuation *) - Option.get (cf ctx)) + cf ctx) see_cf_l in - (* Synthesize *) - let res = S.synthesize_symbolic_expansion sv resl in - (* Return *) - Some res + (* Collect the result: either we computed no subterm, or we computed all + * of them *) + let subterms = + match resl with + | Some _ :: _ -> Some (List.map Option.get resl) + | None :: _ -> + List.iter (fun res -> assert (res = None)) resl; + None + | _ -> failwith "Unreachable" + in + (* Synthesize and return *) + S.synthesize_symbolic_expansion sv subterms (** Expand a symbolic value which is not an enumeration with several variants (i.e., in a situation where it doesn't lead to branching). diff --git a/src/Synthesis.ml b/src/Synthesis.ml index d28a7971..8a0dce93 100644 --- a/src/Synthesis.ml +++ b/src/Synthesis.ml @@ -34,9 +34,9 @@ type synth_function = C.eval_ctx -> synth_function_res in a continuation passing style. *) *) -let synthesize_symbolic_expansion (_sv : V.symbolic_value) (resl : sexpr list) : - sexpr = - SList resl +let synthesize_symbolic_expansion (_sv : V.symbolic_value) + (resl : sexpr list option) : sexpr option = + match resl with None -> None | Some resl -> Some (SList resl) (** Synthesize code for a symbolic expansion which doesn't lead to branching (i.e., applied on a value which is not an enumeration with several variants). |