diff options
| -rw-r--r-- | src/Interpreter.ml | 107 | ||||
| -rw-r--r-- | src/Synthesis.ml | 7 | ||||
| -rw-r--r-- | src/Utils.ml | 6 |
3 files changed, 74 insertions, 46 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index f18124f8..3c8e40b6 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -3877,44 +3877,46 @@ 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 = - (* Synthesis *) - S.synthesize_non_local_function_call fid region_params type_params args dest; - - (* 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 *) - eval_box_free config region_params type_params args dest ctx - | _ -> - (* "Normal" case: not box_free *) - (* Evaluate the operands *) - let ctx, args_vl = eval_operands config ctx args in - - (* Evaluate the function call *) - let ctx, ret_value = - match fid with - | A.BoxNew -> eval_box_new_symbolic config region_params type_params ctx - | A.BoxDeref -> - eval_box_deref_symbolic config region_params type_params ctx - | A.BoxDerefMut -> - eval_box_deref_mut_symbolic config region_params type_params ctx - | A.BoxFree -> failwith "Unreachable" - (* should have been treated above *) - in - - (* Move the return value to its destination *) - let ctx = assign_to_place config ctx ret_value dest in + raise Unimplemented - (* Return *) - ctx +(* (* Synthesis *) + S.synthesize_function_call (A.Assumed fid) region_params type_params args dest; + + (* 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 *) + eval_box_free config region_params type_params args dest ctx + | _ -> + (* "Normal" case: not box_free *) + (* Evaluate the operands *) + let ctx, args_vl = eval_operands config ctx args in + + (* Evaluate the function call *) + let ctx, ret_value = + match fid with + | A.BoxNew -> eval_box_new_symbolic config region_params type_params ctx + | A.BoxDeref -> + eval_box_deref_symbolic config region_params type_params ctx + | A.BoxDerefMut -> + eval_box_deref_mut_symbolic config region_params type_params ctx + | A.BoxFree -> failwith "Unreachable" + (* should have been treated above *) + in + + (* Move the return value to its destination *) + let ctx = assign_to_place config ctx ret_value dest in + + (* Return *) + ctx*) (** Evaluate a non-local (i.e, assumed) function call such as `Box::deref` (auxiliary helper for [eval_statement]) *) @@ -4260,6 +4262,32 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) in (* Substitute the signature *) let inst_sg = Subst.substitute_signature asubst rsubst tsubst sg in + (* TODO: cut from here *) + (* Generate a fresh symbolic value for the return value *) + let ret_sv_ty = inst_sg.A.output in + let ctx, ret_spc = + 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 + (* Sanity check *) + assert (List.length args = def.A.arg_count); + (* Evaluate the function call *) + eval_function_call_symbolic_from_inst_sig config ctx (A.Local fid) inst_sg + region_params type_params args dest + +(** Evaluate a function call in symbolic mode by using the function signature. + + This allows us to factorize the evaluation of local and non-local function + calls in symbolic mode: only their signatures matter. + *) +and eval_function_call_symbolic_from_inst_sig (config : C.config) + (ctx : C.eval_ctx) (fid : A.fun_id) (inst_sg : A.inst_fun_sig) + (region_params : T.erased_region list) (type_params : T.ety list) + (args : E.operand list) (dest : E.place) : C.eval_ctx = (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.A.output in let ctx, ret_spc = @@ -4272,8 +4300,7 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) in (* Evaluate the input operands *) let ctx, args = eval_operands config ctx args in - assert (List.length args = def.A.arg_count); - let args_with_rtypes = List.combine args rtype_params in + let args_with_rtypes = List.combine args inst_sg.A.inputs in (* 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 = let abs_id = rg.A.id in @@ -4307,7 +4334,7 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) (* Move the return value to its destination *) let ctx = assign_to_place config ctx ret_value dest in (* Synthesis *) - S.synthesize_local_function_call fid region_params type_params args dest + S.synthesize_function_call fid region_params type_params args dest ret_spc.V.svalue; (* Return *) ctx diff --git a/src/Synthesis.ml b/src/Synthesis.ml index 60c387d2..1f683209 100644 --- a/src/Synthesis.ml +++ b/src/Synthesis.ml @@ -63,12 +63,7 @@ let synthesize_eval_rvalue_aggregate (aggregate_kind : E.aggregate_kind) (ops : E.operand list) : 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) +let synthesize_function_call (fid : A.fun_id) (region_params : T.erased_region list) (type_params : T.ety list) (args : V.typed_value list) (dest : E.place) (res : V.symbolic_value) : unit = diff --git a/src/Utils.ml b/src/Utils.ml new file mode 100644 index 00000000..a285e869 --- /dev/null +++ b/src/Utils.ml @@ -0,0 +1,6 @@ +exception Found +(** Utility exception + + When looking for something while exploring a term, it can be easier to + just throw an exception to signal we found what we were looking for. + *) |