Make good progress on implementing utilities to test symbolic execution

10 files changed, 269 insertions, 94 deletions

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index a4a128c3..ac66d1a4 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -95,13 +95,19 @@ class ['self] iter_statement_base =
 
     method visit_assertion : 'env -> assertion -> unit = fun _ _ -> ()
 
+    method visit_operand : 'env -> operand -> unit = fun _ _ -> ()
+
     method visit_call : 'env -> call -> unit = fun _ _ -> ()
+
+    method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
+
+    method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> ()
   end
 
 (** Ancestor for [typed_value] map visitor *)
 class ['self] map_statement_base =
   object (_self : 'self)
-    inherit [_] VisitorsRuntime.iter
+    inherit [_] VisitorsRuntime.map
 
     method visit_place : 'env -> place -> place = fun _ x -> x
 
@@ -111,7 +117,15 @@ class ['self] map_statement_base =
 
     method visit_assertion : 'env -> assertion -> assertion = fun _ x -> x
 
+    method visit_operand : 'env -> operand -> operand = fun _ x -> x
+
     method visit_call : 'env -> call -> call = fun _ x -> x
+
+    method visit_integer_type : 'env -> integer_type -> integer_type =
+      fun _ x -> x
+
+    method visit_scalar_value : 'env -> scalar_value -> scalar_value =
+      fun _ x -> x
   end
 
 type statement =
@@ -136,7 +150,6 @@ type statement =
   | Sequence of statement * statement
   | Switch of operand * switch_targets
   | Loop of statement
-[@@deriving show]
 
 and switch_targets =
   | If of statement * statement  (** Gives the "if" and "else" blocks *)
diff --git a/src/CfimAstUtils.ml b/src/CfimAstUtils.ml
index f811475c..96410dde 100644
--- a/src/CfimAstUtils.ml
+++ b/src/CfimAstUtils.ml
@@ -2,7 +2,7 @@ open CfimAst
 open Utils
 
 (** Check if a [statement] contains loops *)
-let rec statement_has_loops (st : statement) : bool =
+let statement_has_loops (st : statement) : bool =
   let obj =
     object
       inherit [_] iter_statement
@@ -14,3 +14,6 @@ let rec statement_has_loops (st : statement) : bool =
     obj#visit_statement () st;
     false
   with Found -> true
+
+(** Check if a [fun_def] contains loops *)
+let fun_def_has_loops (fd : fun_def) : bool = statement_has_loops fd.body
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index e74aa1e7..cb42abf2 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1,4 +1,9 @@
+open Errors
 module L = Logging
+module T = Types
+module A = CfimAst
+open Utils
+open InterpreterUtils
 open InterpreterExpressions
 open InterpreterStatements
 
@@ -18,9 +23,94 @@ open InterpreterStatements
 (* TODO: remove the config parameters when they are useless *)
 
 module Test = struct
+  let initialize_context (type_context : C.type_context)
+      (fun_defs : A.fun_def list) : C.eval_ctx =
+    {
+      C.type_context;
+      C.fun_context = fun_defs;
+      C.type_vars = [];
+      C.env = [];
+      C.symbolic_counter = V.SymbolicValueId.generator_zero;
+      C.borrow_counter = V.BorrowId.generator_zero;
+      C.region_counter = T.RegionId.generator_zero;
+      C.abstraction_counter = V.AbstractionId.generator_zero;
+    }
+
+  (** 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 ⊥
+      "Dummy" abstractions are introduced for the regions present in the
+      function signature.
+   *)
+  let initialize_symbolic_context_for_fun (type_context : C.type_context)
+      (fun_defs : A.fun_def list) (fdef : A.fun_def) : C.eval_ctx =
+    (* 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.
+     * *)
+    (* Create the context *)
+    let ctx = initialize_context type_context fun_defs in
+    (* Instantiate the signature *)
+    let sg = fdef.signature in
+    let type_params =
+      List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params
+    in
+    let ctx, inst_sg = instantiate_fun_sig type_params sg ctx in
+    (* Create fresh symbolic values for the inputs *)
+    let ctx, input_svs =
+      List.fold_left_map
+        (fun ctx ty -> mk_fresh_symbolic_value ty ctx)
+        ctx inst_sg.inputs
+    in
+    (* Create the abstractions and insert them in the context *)
+    let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
+      let abs_id = rg.A.id in
+      let parents =
+        List.fold_left
+          (fun s pid -> V.AbstractionId.Set.add pid s)
+          V.AbstractionId.Set.empty rg.A.parents
+      in
+      let regions =
+        List.fold_left
+          (fun s rid -> T.RegionId.Set.add rid s)
+          T.RegionId.Set.empty rg.A.regions
+      in
+      (* Project over the values - we use *loan* projectors, as explained above *)
+      let avalues = List.map mk_aproj_loans_from_symbolic_value input_svs in
+      (* Create the abstraction *)
+      let abs = { V.abs_id; parents; regions; avalues } in
+      (* Insert the abstraction in the context *)
+      let ctx = { ctx with env = Abs abs :: ctx.env } in
+      (* Return *)
+      ctx
+    in
+    (* Split the variables between return var, inputs and remaining locals *)
+    let ret_var = List.hd fdef.locals in
+    let input_vars, local_vars =
+      list_split_at (List.tl fdef.locals) fdef.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
+
   (** Test a unit function (taking no arguments) by evaluating it in an empty
-    environment
- *)
+      environment.
+   *)
   let test_unit_function (type_context : C.type_context)
       (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : unit eval_result =
     (* Retrieve the function declaration *)
@@ -36,20 +126,9 @@ module Test = struct
     assert (fdef.A.arg_count = 0);
 
     (* Create the evaluation context *)
-    let ctx =
-      {
-        C.type_context;
-        C.fun_context = fun_defs;
-        C.type_vars = [];
-        C.env = [];
-        C.symbolic_counter = V.SymbolicValueId.generator_zero;
-        C.borrow_counter = V.BorrowId.generator_zero;
-        C.region_counter = T.RegionId.generator_zero;
-        C.abstraction_counter = V.AbstractionId.generator_zero;
-      }
-    in
+    let ctx = initialize_context type_context fun_defs in
 
-    (* Put the (uninitialized) local variables *)
+    (* Insert the (uninitialized) local variables *)
     let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in
 
     (* Evaluate the function *)
@@ -70,15 +149,65 @@ module Test = struct
     && List.length def.A.signature.inputs = 0
 
   (** Test all the unit functions in a list of function definitions *)
-  let test_all_unit_functions (type_defs : T.type_def list)
+  let test_unit_functions (type_defs : T.type_def list)
+      (fun_defs : A.fun_def list) : unit =
+    let unit_funs = List.filter fun_def_is_unit fun_defs in
+    let test_unit_fun (def : A.fun_def) : unit =
+      let type_ctx = { C.type_defs } in
+      match test_unit_function type_ctx fun_defs def.A.def_id with
+      | Error _ -> failwith "Unit test failed (concrete execution)"
+      | Ok _ -> ()
+    in
+    List.iter test_unit_fun unit_funs
+
+  (** Execute the symbolic interpreter on a function. *)
+  let test_symbolic_function (type_context : C.type_context)
+      (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : unit eval_result list
+      =
+    (* Retrieve the function declaration *)
+    let fdef = A.FunDefId.nth fun_defs fid in
+
+    (* Debug *)
+    L.log#ldebug
+      (lazy
+        ("test_symbolic_function: " ^ Print.Types.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 (fdef.A.arg_count = 0);
+
+    (* Create the evaluation context *)
+    let ctx = initialize_context type_context fun_defs in
+
+    (* Initialize the inputs as symbolic values *)
+    raise Unimplemented
+
+  (* (* Initialize the remaining local variables as Bottom *)
+     let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in
+
+     (* Evaluate the function *)
+     let config = { C.mode = C.ConcreteMode; C.check_invariants = true } 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"*)
+
+  (** 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_symbolic_functions (type_defs : T.type_def list)
       (fun_defs : A.fun_def list) : unit =
+    let no_loop_funs = List.filter CfimAstUtils.fun_def_has_loops fun_defs in
     let test_fun (def : A.fun_def) : unit =
-      if fun_def_is_unit def then
-        let type_ctx = { C.type_defs } in
-        match test_unit_function type_ctx fun_defs def.A.def_id with
-        | Error _ -> failwith "Unit test failed"
-        | Ok _ -> ()
-      else ()
+      let type_ctx = { C.type_defs } in
+      let res = test_symbolic_function type_ctx fun_defs def.A.def_id in
+      if List.for_all Result.is_ok res then ()
+      else failwith "Unit test failed (symbolic execution)"
     in
     List.iter test_fun fun_defs
 end
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index d4de318b..80725bab 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -410,7 +410,7 @@ let expand_bottom_value_from_projection (config : C.config)
      during whose evaluation we got stuck *)
   let projection' =
     fst
-      (Utilities.list_split_at p.projection
+      (Utils.list_split_at p.projection
          (List.length p.projection - remaining_pes))
   in
   let p' = { p with projection = projection' } in
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 91035574..6b06a27f 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -421,6 +421,54 @@ let eval_non_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
           (* Return *)
           Ok ctx)
 
+(** Instantiate a function signature, introducing fresh abstraction ids and
+    region ids. This is mostly used in preparation of function calls, when
+    evaluating in symbolic mode of course.
+    
+    Note: there are no region parameters, because they should be erased.
+ *)
+let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig)
+    (ctx : C.eval_ctx) : C.eval_ctx * A.inst_fun_sig =
+  (* Generate fresh abstraction ids and create a substitution from region
+   * group ids to abstraction ids *)
+  let ctx, rg_abs_ids_bindings =
+    List.fold_left_map
+      (fun ctx rg ->
+        let ctx, abs_id = C.fresh_abstraction_id ctx in
+        (ctx, (rg.A.id, abs_id)))
+      ctx sg.regions_hierarchy
+  in
+  let asubst_map : V.AbstractionId.id A.RegionGroupId.Map.t =
+    List.fold_left
+      (fun mp (rg_id, abs_id) -> A.RegionGroupId.Map.add rg_id abs_id mp)
+      A.RegionGroupId.Map.empty rg_abs_ids_bindings
+  in
+  let asubst (rg_id : A.RegionGroupId.id) : V.AbstractionId.id =
+    A.RegionGroupId.Map.find rg_id asubst_map
+  in
+  (* Generate fresh regions and their substitutions *)
+  let ctx, _, rsubst, _ =
+    Subst.fresh_regions_with_substs sg.region_params ctx
+  in
+  (* Generate the type substitution
+   * Note that we need the substitution to map the type variables to
+   * [rty] types (not [ety]). In order to do that, we convert the
+   * type parameters to types with regions. This is possible only
+   * if those types don't contain any regions.
+   * This is a current limitation of the analysis: there is still some
+   * work to do to properly handle full type parametrization.
+   * *)
+  let rtype_params = List.map ety_no_regions_to_rty type_params in
+  let tsubst =
+    Subst.make_type_subst
+      (List.map (fun v -> v.T.index) sg.type_params)
+      rtype_params
+  in
+  (* Substitute the signature *)
+  let inst_sig = Subst.substitute_signature asubst rsubst tsubst sg in
+  (* Return *)
+  (ctx, inst_sig)
+
 (** Evaluate a statement *)
 let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
     : (C.eval_ctx * statement_eval_res) eval_result list =
@@ -661,7 +709,7 @@ and eval_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
   let ctx = C.ctx_push_var ctx ret_var (C.mk_bottom ret_var.var_ty) in
 
   (* 2. Push the input values *)
-  let input_locals, locals = Utilities.list_split_at locals def.A.arg_count in
+  let input_locals, locals = Utils.list_split_at locals def.A.arg_count in
   let inputs = List.combine input_locals args in
   (* Note that this function checks that the variables and their values
      have the same type (this is important) *)
@@ -697,43 +745,9 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
   (* Retrieve the (correctly instantiated) signature *)
   let def = C.ctx_lookup_fun_def ctx fid in
   let sg = def.A.signature in
-  (* Generate fresh abstraction ids and create a substitution from region
-   * group ids to abstraction ids *)
-  let ctx, rg_abs_ids_bindings =
-    List.fold_left_map
-      (fun ctx rg ->
-        let ctx, abs_id = C.fresh_abstraction_id ctx in
-        (ctx, (rg.A.id, abs_id)))
-      ctx sg.regions_hierarchy
-  in
-  let asubst_map : V.AbstractionId.id A.RegionGroupId.Map.t =
-    List.fold_left
-      (fun mp (rg_id, abs_id) -> A.RegionGroupId.Map.add rg_id abs_id mp)
-      A.RegionGroupId.Map.empty rg_abs_ids_bindings
-  in
-  let asubst (rg_id : A.RegionGroupId.id) : V.AbstractionId.id =
-    A.RegionGroupId.Map.find rg_id asubst_map
-  in
-  (* Generate fresh regions and their substitutions *)
-  let ctx, _, rsubst, _ =
-    Subst.fresh_regions_with_substs sg.region_params ctx
-  in
-  (* Generate the type substitution
-   * Note that we need the substitution to map the type variables to
-   * [rty] types (not [ety]). In order to do that, we convert the
-   * type parameters to types with regions. This is possible only
-   * if those types don't contain any regions.
-   * This is a current limitation of the analysis: there is still some
-   * work to do to properly handle full type parametrization.
-   * *)
-  let rtype_params = List.map ety_no_regions_to_rty type_params in
-  let tsubst =
-    Subst.make_type_subst
-      (List.map (fun v -> v.T.index) sg.type_params)
-      rtype_params
-  in
-  (* Substitute the signature *)
-  let inst_sg = Subst.substitute_signature asubst rsubst tsubst sg in
+  (* Instantiate the signature and introduce fresh abstraction and region ids
+   * while doing so *)
+  let ctx, inst_sg = instantiate_fun_sig type_params sg ctx in
   (* Sanity check *)
   assert (List.length args = def.A.arg_count);
   (* Evaluate the function call *)
@@ -755,10 +769,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     mk_fresh_symbolic_proj_comp T.RegionId.Set.empty ret_sv_ty ctx
   in
   let ret_value = mk_typed_value_from_proj_comp ret_spc in
-  let ret_av = V.ASymbolic (V.AProjLoans ret_spc.V.svalue) in
-  let ret_av : V.typed_avalue =
-    { V.value = ret_av; V.ty = ret_spc.V.svalue.V.sv_ty }
-  in
+  let ret_av = mk_aproj_loans_from_symbolic_value ret_spc.V.svalue in
   (* Evaluate the input operands *)
   let ctx, args = eval_operands config ctx args in
   let args_with_rtypes = List.combine args inst_sg.A.inputs in
@@ -768,8 +779,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
       (fun ((arg, rty) : V.typed_value * T.rty) ->
         arg.V.ty = Subst.erase_regions rty)
       args_with_rtypes);
-  (* Generate the abstractions from the region groups and add them to the context *)
-  let gen_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
+  (* Create the abstractions from the region groups and add them to the context *)
+  let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
     let abs_id = rg.A.id in
     let parents =
       List.fold_left
@@ -797,7 +808,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     (* Return *)
     ctx
   in
-  let ctx = List.fold_left gen_abs ctx inst_sg.A.regions_hierarchy in
+  let ctx = List.fold_left create_abs ctx inst_sg.A.regions_hierarchy in
   (* Move the return value to its destination *)
   let ctx = assign_to_place config ctx ret_value dest in
   (* Synthesis *)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 5e0375d0..cc54cd24 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -37,11 +37,17 @@ let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : A.var
 let mk_place_from_var_id (var_id : V.VarId.id) : E.place =
   { var_id; projection = [] }
 
+(** Create a fresh symbolic value *)
+let mk_fresh_symbolic_value (ty : T.rty) (ctx : C.eval_ctx) :
+    C.eval_ctx * V.symbolic_value =
+  let ctx, sv_id = C.fresh_symbolic_value_id ctx in
+  let svalue = { V.sv_id; V.sv_ty = ty } in
+  (ctx, svalue)
+
 (** Create a fresh symbolic proj comp *)
 let mk_fresh_symbolic_proj_comp (ended_regions : T.RegionId.set_t) (ty : T.rty)
     (ctx : C.eval_ctx) : C.eval_ctx * V.symbolic_proj_comp =
-  let ctx, sv_id = C.fresh_symbolic_value_id ctx in
-  let svalue = { V.sv_id; V.sv_ty = ty } in
+  let ctx, svalue = mk_fresh_symbolic_value ty ctx in
   let sv = { V.svalue; rset_ended = ended_regions } in
   (ctx, sv)
 
@@ -64,12 +70,24 @@ let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
   let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in
   mk_typed_value_from_proj_comp spc
 
-let mk_aproj_loans_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_avalue =
-  let ty = sv.V.svalue.V.sv_ty in
-  let proj = V.AProjLoans sv.V.svalue in
+let mk_aproj_loans_from_proj_comp (spc : V.symbolic_proj_comp) : V.typed_avalue
+    =
+  let ty = spc.V.svalue.V.sv_ty in
+  let proj = V.AProjLoans spc.V.svalue in
   let value = V.ASymbolic proj in
   { V.value; ty }
 
+(** Create a Loans projector from a symbolic value.
+
+    Initializes the set of ended regions with `empty`.
+ *)
+let mk_aproj_loans_from_symbolic_value (svalue : V.symbolic_value) :
+    V.typed_avalue =
+  let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in
+  let av = V.ASymbolic (V.AProjLoans spc.V.svalue) in
+  let av : V.typed_avalue = { V.value = av; V.ty = svalue.V.sv_ty } in
+  av
+
 (** TODO: move *)
 let borrow_is_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrow) : bool
     =
diff --git a/src/Print.ml b/src/Print.ml
index 90f3946b..de1952e1 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -843,7 +843,7 @@ module CfimAst = struct
 
     (* Arguments *)
     let inputs = List.tl def.locals in
-    let inputs, _aux_locals = Utilities.list_split_at inputs def.arg_count in
+    let inputs, _aux_locals = Utils.list_split_at inputs def.arg_count in
     let args = List.combine inputs sg.inputs in
     let args =
       List.map
diff --git a/src/Utilities.ml b/src/Utilities.ml
deleted file mode 100644
index 6452d56f..00000000
--- a/src/Utilities.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-(* Split a list at a given index [i] (the first list contains all the elements
-   up to element of index [i], not included, the second one contains the remaining
-   elements. Note that the first returned list has length [i].
- *)
-let rec list_split_at (ls : 'a list) (i : int) =
-  if i < 0 then raise (Invalid_argument "list_split_at take positive integers")
-  else if i = 0 then ([], ls)
-  else
-    match ls with
-    | [] ->
-        raise
-          (Failure
-             "The int given to list_split_at should be <= the list's length")
-    | x :: ls' ->
-        let ls1, ls2 = list_split_at ls' (i - 1) in
-        (x :: ls1, ls2)
diff --git a/src/Utils.ml b/src/Utils.ml
index a285e869..16ee7252 100644
--- a/src/Utils.ml
+++ b/src/Utils.ml
@@ -1,3 +1,20 @@
+(* Split a list at a given index [i] (the first list contains all the elements
+   up to element of index [i], not included, the second one contains the remaining
+   elements. Note that the first returned list has length [i].
+*)
+let rec list_split_at (ls : 'a list) (i : int) =
+  if i < 0 then raise (Invalid_argument "list_split_at take positive integers")
+  else if i = 0 then ([], ls)
+  else
+    match ls with
+    | [] ->
+        raise
+          (Failure
+             "The int given to list_split_at should be <= the list's length")
+    | x :: ls' ->
+        let ls1, ls2 = list_split_at ls' (i - 1) in
+        (x :: ls1, ls2)
+
 exception Found
 (** Utility exception
 
diff --git a/src/main.ml b/src/main.ml
index 2d2518c7..b4537c3a 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -46,4 +46,4 @@ let () =
       log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
 
       (* Test the unit functions *)
-      I.Test.test_all_unit_functions m.types m.functions
+      I.Test.test_unit_functions m.types m.functions