Fix a mistake with the input symbolic values not being linked to the

input variables when translating ASTs from symbolic to pure

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 =