From 7e7d0d67de8285e1d6c589750191bce4f49aacb3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 27 Oct 2022 09:16:46 +0200
Subject: Reorganize a bit the project

---
 compiler/Interpreter.ml | 396 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 396 insertions(+)
 create mode 100644 compiler/Interpreter.ml

(limited to 'compiler/Interpreter.ml')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
new file mode 100644
index 00000000..7f51c5b9
--- /dev/null
+++ b/compiler/Interpreter.ml
@@ -0,0 +1,396 @@
+open Cps
+open InterpreterUtils
+open InterpreterProjectors
+open InterpreterBorrows
+open InterpreterStatements
+open LlbcAstUtils
+module L = Logging
+module T = Types
+module A = LlbcAst
+module SA = SymbolicAst
+
+(** The local logger *)
+let log = L.interpreter_log
+
+let compute_type_fun_global_contexts (m : Crates.llbc_crate) :
+    C.type_context * C.fun_context * C.global_context =
+  let type_decls_list, _, _ = Crates.split_declarations m.declarations in
+  let type_decls, fun_decls, global_decls = Crates.compute_defs_maps m in
+  let type_decls_groups, _funs_defs_groups, _globals_defs_groups =
+    Crates.split_declarations_to_group_maps m.declarations
+  in
+  let type_infos =
+    TypesAnalysis.analyze_type_declarations type_decls type_decls_list
+  in
+  let type_context = { C.type_decls_groups; type_decls; type_infos } in
+  let fun_context = { C.fun_decls } in
+  let global_context = { C.global_decls } in
+  (type_context, fun_context, global_context)
+
+let initialize_eval_context (type_context : C.type_context)
+    (fun_context : C.fun_context) (global_context : C.global_context)
+    (type_vars : T.type_var list) : C.eval_ctx =
+  C.reset_global_counters ();
+  {
+    C.type_context;
+    C.fun_context;
+    C.global_context;
+    C.type_vars;
+    C.env = [ C.Frame ];
+    C.ended_regions = T.RegionId.Set.empty;
+  }
+
+(** Initialize an evaluation context to execute a function.
+
+      Introduces local variables initialized in the following manner:
+      - input arguments are initialized as symbolic values
+      - 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) (global_context : C.global_context)
+    (fdef : A.fun_decl) : 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
+   * by some function calls...).
+   * Also, note that we properly set the set of parents of every abstraction:
+   * this should not be necessary, as those abstractions should never be
+   * *automatically* ended (because ending some borrows requires to end
+   * one of them), but rather selectively ended when generating code
+   * for each of the backward functions. We do it only because we can
+   * do it, and because it gives a bit of sanity.
+   * *)
+  let sg = fdef.signature in
+  (* Create the context *)
+  let ctx =
+    initialize_eval_context type_context fun_context global_context
+      sg.type_params
+  in
+  (* Instantiate the signature *)
+  let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in
+  let inst_sg = instantiate_fun_sig type_params sg in
+  (* Create fresh symbolic values for the inputs *)
+  let input_svs =
+    List.map (fun ty -> mk_fresh_symbolic_value V.SynthInput ty) inst_sg.inputs
+  in
+  (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
+  let call_id = C.fresh_fun_call_id () in
+  assert (call_id = V.FunCallId.zero);
+  let compute_abs_avalues (abs : V.abs) (ctx : C.eval_ctx) :
+      C.eval_ctx * V.typed_avalue list =
+    (* Project over the values - we use *loan* projectors, as explained above *)
+    let avalues =
+      List.map (mk_aproj_loans_value_from_symbolic_value abs.regions) input_svs
+    in
+    (ctx, avalues)
+  in
+  let region_can_end _ = true in
+  let ctx =
+    create_push_abstractions_from_abs_region_groups call_id V.SynthInput
+      inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
+  in
+  (* Split the variables between return var, inputs and remaining locals *)
+  let body = Option.get fdef.body in
+  let ret_var = List.hd body.locals in
+  let input_vars, local_vars =
+    Collections.List.split_at (List.tl body.locals) body.arg_count
+  in
+  (* Push the return variable (initialized with ⊥) *)
+  let ctx = C.ctx_push_uninitialized_var ctx ret_var in
+  (* Push the input variables (initialized with symbolic values) *)
+  let input_values = List.map mk_typed_value_from_symbolic_value input_svs in
+  let ctx = C.ctx_push_vars ctx (List.combine input_vars input_values) in
+  (* Push the remaining local variables (initialized with ⊥) *)
+  let ctx = C.ctx_push_uninitialized_vars ctx local_vars in
+  (* Return *)
+  (ctx, input_svs, inst_sg)
+
+(** Small helper.
+
+    This is a continuation function called by the symbolic interpreter upon
+    reaching the [return] instruction when synthesizing a *backward* function:
+    this continuation takes care of doing the proper manipulations to finish
+    the synthesis (mostly by ending abstractions).
+*)
+let evaluate_function_symbolic_synthesize_backward_from_return
+    (config : C.config) (fdef : A.fun_decl) (inst_sg : A.inst_fun_sig)
+    (back_id : T.RegionGroupId.id) (ctx : C.eval_ctx) : SA.expression option =
+  (* We need to instantiate the function signature - to retrieve
+   * the return type. Note that it is important to re-generate
+   * an instantiation of the signature, so that we use fresh
+   * region ids for the return abstractions. *)
+  let sg = fdef.signature in
+  let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in
+  let ret_inst_sg = instantiate_fun_sig type_params sg in
+  let ret_rty = ret_inst_sg.output in
+  (* Move the return value out of the return variable *)
+  let cf_pop_frame = ctx_pop_frame config in
+
+  (* We need to find the parents regions/abstractions of the region we
+   * will end - this will allow us to, first, mark the other return
+   * regions as non-endable, and, second, end those parent regions in
+   * proper order. *)
+  let parent_rgs = list_parent_region_groups sg back_id in
+  let parent_input_abs_ids =
+    T.RegionGroupId.mapi
+      (fun rg_id rg ->
+        if T.RegionGroupId.Set.mem rg_id parent_rgs then Some rg.T.id else None)
+      inst_sg.regions_hierarchy
+  in
+  let parent_input_abs_ids =
+    List.filter_map (fun x -> x) parent_input_abs_ids
+  in
+
+  (* Insert the return value in the return abstractions (by applying
+   * borrow projections) *)
+  let cf_consume_ret ret_value ctx =
+    let ret_call_id = C.fresh_fun_call_id () in
+    let compute_abs_avalues (abs : V.abs) (ctx : C.eval_ctx) :
+        C.eval_ctx * V.typed_avalue list =
+      let ctx, avalue =
+        apply_proj_borrows_on_input_value config ctx abs.regions
+          abs.ancestors_regions ret_value ret_rty
+      in
+      (ctx, [ avalue ])
+    in
+
+    (* Initialize and insert the abstractions in the context.
+     *
+     * We take care of disallowing ending the return regions which we
+     * shouldn't end (see the documentation of the [can_end] field of [abs]
+     * for more information. *)
+    let parent_and_current_rgs = T.RegionGroupId.Set.add back_id parent_rgs in
+    let region_can_end rid =
+      T.RegionGroupId.Set.mem rid parent_and_current_rgs
+    in
+    assert (region_can_end back_id);
+    let ctx =
+      create_push_abstractions_from_abs_region_groups ret_call_id V.SynthRet
+        ret_inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
+    in
+
+    (* We now need to end the proper *input* abstractions - pay attention
+     * to the fact that we end the *input* abstractions, not the *return*
+     * abstractions (of course, the corresponding return abstractions will
+     * automatically be ended, because they consumed values coming from the
+     * input abstractions...) *)
+    (* End the parent abstractions and the current abstraction - note that we
+     * end them in an order which follows the regions hierarchy: it should lead
+     * to generated code which has a better consistency between the parent
+     * and children backward functions *)
+    let current_abs_id =
+      (T.RegionGroupId.nth inst_sg.regions_hierarchy back_id).id
+    in
+    let target_abs_ids = List.append parent_input_abs_ids [ current_abs_id ] in
+    let cf_end_target_abs cf =
+      List.fold_left
+        (fun cf id -> end_abstraction config [] id cf)
+        cf target_abs_ids
+    in
+    (* Generate the Return node *)
+    let cf_return : m_fun = fun _ -> Some (SA.Return None) in
+    (* Apply *)
+    cf_end_target_abs cf_return ctx
+  in
+  cf_pop_frame cf_consume_ret ctx
+
+(** 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)
+    (global_context : C.global_context) (fdef : A.fun_decl)
+    (back_id : T.RegionGroupId.id option) :
+    V.symbolic_value list * SA.expression option =
+  (* Debug *)
+  let name_to_string () =
+    Print.fun_name_to_string fdef.A.name
+    ^ " ("
+    ^ Print.option_to_string T.RegionGroupId.to_string back_id
+    ^ ")"
+  in
+  log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ()));
+
+  (* Create the evaluation context *)
+  let ctx, input_svs, inst_sg =
+    initialize_symbolic_context_for_fun type_context fun_context global_context
+      fdef
+  in
+
+  (* Create the continuation to finish the evaluation *)
+  let config = C.config_of_partial C.SymbolicMode config in
+  let cf_finish res ctx =
+    match res with
+    | Return ->
+        if synthesize then
+          (* There are two cases:
+           * - if this is a forward translation, we retrieve the returned value.
+           * - if this is a backward translation, we introduce "return"
+           *   abstractions to consume the return value, then end all the
+           *   abstractions up to the one in which we are interested.
+           *)
+          match back_id with
+          | None ->
+              (* Forward translation *)
+              (* Pop the frame and retrieve the returned value at the same time*)
+              let cf_pop = ctx_pop_frame config in
+              (* Generate the Return node *)
+              let cf_return ret_value : m_fun =
+               fun _ -> Some (SA.Return (Some ret_value))
+              in
+              (* Apply *)
+              cf_pop cf_return ctx
+          | Some back_id ->
+              (* Backward translation *)
+              evaluate_function_symbolic_synthesize_backward_from_return config
+                fdef inst_sg back_id ctx
+        else None
+    | Panic ->
+        (* Note that as we explore all the execution branches, one of
+         * the executions can lead to a panic *)
+        if synthesize then Some SA.Panic else None
+    | _ ->
+        failwith ("evaluate_function_symbolic failed on: " ^ name_to_string ())
+  in
+
+  (* Evaluate the function *)
+  let symbolic =
+    eval_function_body config (Option.get fdef.A.body).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
+      environment.
+   *)
+  let test_unit_function (config : C.partial_config) (crate : Crates.llbc_crate)
+      (fid : A.FunDeclId.id) : unit =
+    (* Retrieve the function declaration *)
+    let fdef = A.FunDeclId.nth crate.functions fid in
+    let body = Option.get fdef.body in
+
+    (* Debug *)
+    log#ldebug
+      (lazy ("test_unit_function: " ^ Print.fun_name_to_string fdef.A.name));
+
+    (* Sanity check - *)
+    assert (List.length fdef.A.signature.region_params = 0);
+    assert (List.length fdef.A.signature.type_params = 0);
+    assert (body.A.arg_count = 0);
+
+    (* Create the evaluation context *)
+    let type_context, fun_context, global_context =
+      compute_type_fun_global_contexts crate
+    in
+    let ctx =
+      initialize_eval_context type_context fun_context global_context []
+    in
+
+    (* Insert the (uninitialized) local variables *)
+    let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in
+
+    (* Create the continuation to check the function's result *)
+    let config = C.config_of_partial C.ConcreteMode config in
+    let cf_check res ctx =
+      match res with
+      | Return ->
+          (* Ok: drop the local variables and finish *)
+          ctx_pop_frame config (fun _ _ -> None) ctx
+      | _ ->
+          failwith
+            ("Unit test failed (concrete execution) on: "
+            ^ Print.fun_name_to_string fdef.A.name)
+    in
+
+    (* Evaluate the function *)
+    let _ = eval_function_body config body.body cf_check ctx in
+    ()
+
+  (** Small helper: return true if the function is a *transparent* unit function
+      (no parameters, no arguments) - TODO: move *)
+  let fun_decl_is_transparent_unit (def : A.fun_decl) : bool =
+    match def.body with
+    | None -> false
+    | Some body ->
+        body.arg_count = 0
+        && List.length def.A.signature.region_params = 0
+        && List.length def.A.signature.type_params = 0
+        && List.length def.A.signature.inputs = 0
+
+  (** Test all the unit functions in a list of function definitions *)
+  let test_unit_functions (config : C.partial_config)
+      (crate : Crates.llbc_crate) : unit =
+    let unit_funs = List.filter fun_decl_is_transparent_unit crate.functions in
+    let test_unit_fun (def : A.fun_decl) : unit =
+      test_unit_function config crate 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) (synthesize : bool)
+      (type_context : C.type_context) (fun_context : C.fun_context)
+      (global_context : C.global_context) (fdef : A.fun_decl) : unit =
+    (* Debug *)
+    log#ldebug
+      (lazy ("test_function_symbolic: " ^ Print.fun_name_to_string fdef.A.name));
+
+    (* Evaluate *)
+    let evaluate =
+      evaluate_function_symbolic config synthesize type_context fun_context
+        global_context fdef
+    in
+    (* Execute the forward function *)
+    let _ = evaluate None in
+    (* Execute the backward functions *)
+    let _ =
+      T.RegionGroupId.mapi
+        (fun gid _ -> evaluate (Some gid))
+        fdef.signature.regions_hierarchy
+    in
+
+    ()
+
+  (** Small helper *)
+  let fun_decl_is_transparent (def : A.fun_decl) : bool =
+    Option.is_some def.body
+
+  (** Execute the symbolic interpreter on a list of functions.
+
+      TODO: for now we ignore the functions which contain loops, because
+      they are not supported by the symbolic interpreter.
+   *)
+  let test_functions_symbolic (config : C.partial_config) (synthesize : bool)
+      (crate : Crates.llbc_crate) : unit =
+    (* Filter the functions which contain loops *)
+    let no_loop_funs =
+      List.filter
+        (fun f -> not (LlbcAstUtils.fun_decl_has_loops f))
+        crate.functions
+    in
+    (* Filter the opaque functions *)
+    let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in
+    let type_context, fun_context, global_context =
+      compute_type_fun_global_contexts crate
+    in
+    let test_fun (def : A.fun_decl) : unit =
+      (* 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 *)
+      test_function_symbolic config synthesize type_context fun_context
+        global_context def
+    in
+    List.iter test_fun no_loop_funs
+end
-- 
cgit v1.2.3