Add more calls to synthesis functions

2 files changed, 65 insertions, 1 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index d7004371..1107ee20 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -3359,6 +3359,7 @@ let rec end_loan_exactly_at_place (config : C.config) (access : access_kind)
 let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place)
     (variant_id : T.VariantId.id) :
     (C.eval_ctx * statement_eval_res) eval_result =
+  S.synthesize_set_discriminant p variant_id;
   (* Access the value *)
   let access = Write in
   let ctx = update_ctx_along_read_place config access p ctx in
@@ -3633,6 +3634,9 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx)
        ^ "\n- type_params: " ^ type_params ^ "\n- args: " ^ args ^ "\n- dest: "
        ^ dest));
 
+  (* Synthesis *)
+  S.synthesize_non_local_function_call fid region_params type_params args dest;
+
   (* There are two cases (and this is extremely annoying):
      - the function is not box_free
      - the function is box_free
@@ -3816,9 +3820,10 @@ and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) :
 (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for
     [eval_statement]) *)
 and eval_local_function_call (config : C.config) (ctx : C.eval_ctx)
-    (fid : A.FunDefId.id) (_region_params : T.erased_region list)
+    (fid : A.FunDefId.id) (region_params : T.erased_region list)
     (type_params : T.ety list) (args : E.operand list) (dest : E.place) :
     C.eval_ctx eval_result =
+  S.synthesize_local_function_call fid region_params type_params args dest;
   (* Retrieve the (correctly instantiated) body *)
   let def = C.ctx_lookup_fun_def ctx fid in
   match config.mode with
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
new file mode 100644
index 00000000..85029a58
--- /dev/null
+++ b/src/Synthesis.ml
@@ -0,0 +1,59 @@
+module T = Types
+module V = Values
+open Scalars
+module E = Expressions
+open Errors
+module C = Contexts
+module Subst = Substitute
+module A = CfimAst
+module L = Logging
+open TypesUtils
+open ValuesUtils
+module Inv = Invariants
+open InterpreterUtils
+
+(* TODO: the below functions have very "rough" signatures and do nothing: I
+ * defined them so that the places where we should update the synthesized
+ * program are clearly indicated in Interpreter.ml.
+ *
+ * Small rk.: most functions should take an additional parameter for the
+ * fresh symbolic value which stores the result of the computation.
+ * For instance:
+ *   `synthesize_binary_op Add op1 op2 s`
+ * should generate:
+ *   `s := op1 + op2`
+ * *)
+
+(** TODO: rename to synthesize_symbolic_expansion_{non_enum,one_variant}? *)
+let synthesize_symbolic_expansion (sv : V.symbolic_value)
+    (see : symbolic_expansion) : unit =
+  ()
+
+let synthesize_unary_op (unop : E.unop) (op : E.operand) : unit = ()
+
+let synthesize_binary_op (binop : E.binop) (op1 : E.operand) (op2 : E.operand) :
+    unit =
+  ()
+
+(** Actually not sure if we need this, or a synthesize_symbolic_expansion_enum *)
+let synthesize_eval_rvalue_discriminant (p : E.place) : unit = ()
+
+let synthesize_eval_rvalue_ref (p : E.place) (bkind : E.borrow_kind) : unit = ()
+
+let synthesize_eval_rvalue_aggregate (aggregate_kind : E.aggregate_kind)
+    (ops : E.operand list) : unit =
+  ()
+
+let synthesize_set_discriminant (p : E.place) (variant_id : T.VariantId.id) :
+    unit =
+  ()
+
+let synthesize_non_local_function_call (fid : A.assumed_fun_id)
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (args : E.operand list) (dest : E.place) : unit =
+  ()
+
+let synthesize_local_function_call (fid : A.FunDefId.id)
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (args : E.operand list) (dest : E.place) : unit =
+  ()