summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-05 19:55:47 +0100
committerSon Ho2022-01-05 19:55:47 +0100
commite2a6d69a125f7a4510eecd79c01d3420bb561a9d (patch)
tree6fa2d8d79b2099c9766bf5aa35f303c5ff2ce9f2
parentde4a2300b734e9ea9c29a160a968110507d7747f (diff)
Finish implementing evaluation of non-local function calls in symbolic
mode
-rw-r--r--src/Interpreter.ml140
1 files changed, 71 insertions, 69 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 50b53a67..da72d3c3 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -3906,75 +3906,6 @@ let eval_non_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
(* Return *)
Ok ctx)
-(** Evaluate a non-local function call in concrete mode *)
-let eval_non_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
- (fid : A.assumed_fun_id) (region_params : T.erased_region list)
- (type_params : T.ety list) (args : E.operand list) (dest : E.place) :
- C.eval_ctx =
- (* Sanity check: make sure the type parameters don't contain regions -
- * this is a current limitation of our synthesis *)
- assert (List.for_all (fun ty -> not (ty_has_regions ty)) type_params);
-
- (* There are two cases (and this is extremely annoying):
- - the function is not box_free
- - the function is box_free
- See [eval_box_free]
- *)
- match fid with
- | A.BoxFree ->
- (* Degenerate case: box_free - note that this is not really a function
- * call *)
- eval_box_free config region_params type_params args dest ctx
- | _ ->
- (* "Normal" case: not box_free *)
- (* In symbolic mode, the behaviour of a function call is completely defined
- * by the signature of the function: we thus simply generate correctly
- * instantiated signatures, and delegate the work to an auxiliary function *)
- let ctx, inst_sig =
- match fid with
- | A.BoxNew ->
- (ctx, eval_box_new_inst_sig config region_params type_params)
- | A.BoxDeref ->
- eval_box_deref_inst_sig config region_params type_params ctx
- | A.BoxDerefMut ->
- eval_box_deref_mut_inst_sig config region_params type_params ctx
- | A.BoxFree -> failwith "Unreachable"
- (* should have been treated above *)
- in
-
- raise Unimplemented
-
-(** Evaluate a non-local (i.e, assumed) function call such as `Box::deref`
- (auxiliary helper for [eval_statement]) *)
-let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx)
- (fid : A.assumed_fun_id) (region_params : T.erased_region list)
- (type_params : T.ety list) (args : E.operand list) (dest : E.place) :
- C.eval_ctx eval_result =
- (* Debug *)
- L.log#ldebug
- (lazy
- (let type_params =
- "["
- ^ String.concat ", " (List.map (ety_to_string ctx) type_params)
- ^ "]"
- in
- let args =
- "[" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "]"
- in
- let dest = place_to_string ctx dest in
- "eval_non_local_function_call:\n- fid:" ^ A.show_assumed_fun_id fid
- ^ "\n- type_params: " ^ type_params ^ "\n- args: " ^ args ^ "\n- dest: "
- ^ dest));
-
- match config.mode with
- | C.ConcreteMode ->
- eval_non_local_function_call_concrete config ctx fid region_params
- type_params args dest
- | C.SymbolicMode ->
- Ok
- (eval_non_local_function_call_symbolic config ctx fid region_params
- type_params args dest)
-
(** 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 =
@@ -4360,6 +4291,77 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
(* Return *)
ctx
+(** Evaluate a non-local function call in symbolic mode *)
+and eval_non_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
+ (fid : A.assumed_fun_id) (region_params : T.erased_region list)
+ (type_params : T.ety list) (args : E.operand list) (dest : E.place) :
+ C.eval_ctx =
+ (* Sanity check: make sure the type parameters don't contain regions -
+ * this is a current limitation of our synthesis *)
+ assert (List.for_all (fun ty -> not (ty_has_regions ty)) type_params);
+
+ (* There are two cases (and this is extremely annoying):
+ - the function is not box_free
+ - the function is box_free
+ See [eval_box_free]
+ *)
+ match fid with
+ | A.BoxFree ->
+ (* Degenerate case: box_free - note that this is not really a function
+ * call: no need to call a "synthesize_..." function *)
+ eval_box_free config region_params type_params args dest ctx
+ | _ ->
+ (* "Normal" case: not box_free *)
+ (* In symbolic mode, the behaviour of a function call is completely defined
+ * by the signature of the function: we thus simply generate correctly
+ * instantiated signatures, and delegate the work to an auxiliary function *)
+ let ctx, inst_sig =
+ match fid with
+ | A.BoxNew ->
+ (ctx, eval_box_new_inst_sig config region_params type_params)
+ | A.BoxDeref ->
+ eval_box_deref_inst_sig config region_params type_params ctx
+ | A.BoxDerefMut ->
+ eval_box_deref_mut_inst_sig config region_params type_params ctx
+ | A.BoxFree -> failwith "Unreachable"
+ (* should have been treated above *)
+ in
+
+ (* Evaluate the function call *)
+ eval_function_call_symbolic_from_inst_sig config ctx (A.Assumed fid)
+ inst_sig region_params type_params args dest
+
+(** Evaluate a non-local (i.e, assumed) function call such as `Box::deref`
+ (auxiliary helper for [eval_statement]) *)
+and eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx)
+ (fid : A.assumed_fun_id) (region_params : T.erased_region list)
+ (type_params : T.ety list) (args : E.operand list) (dest : E.place) :
+ C.eval_ctx eval_result =
+ (* Debug *)
+ L.log#ldebug
+ (lazy
+ (let type_params =
+ "["
+ ^ String.concat ", " (List.map (ety_to_string ctx) type_params)
+ ^ "]"
+ in
+ let args =
+ "[" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "]"
+ in
+ let dest = place_to_string ctx dest in
+ "eval_non_local_function_call:\n- fid:" ^ A.show_assumed_fun_id fid
+ ^ "\n- type_params: " ^ type_params ^ "\n- args: " ^ args ^ "\n- dest: "
+ ^ dest));
+
+ match config.mode with
+ | C.ConcreteMode ->
+ eval_non_local_function_call_concrete config ctx fid region_params
+ type_params args dest
+ | C.SymbolicMode ->
+ Ok
+ (eval_non_local_function_call_symbolic config ctx fid region_params
+ type_params args dest)
+
(** 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)