diff options
author | Son Ho | 2024-05-24 16:32:59 +0200 |
---|---|---|
committer | Son Ho | 2024-05-24 16:32:59 +0200 |
commit | 321263384bb1e6e8bfd08806f35164bdba387d74 (patch) | |
tree | 04d90b72b7591e380079614a4335e9ca7fe11268 /compiler/InterpreterStatements.ml | |
parent | 765cb792916c1c69f864a6cf59a49c504ad603a2 (diff) | |
parent | 0baa0519cf477fe1fa447417585960fc811bcae9 (diff) |
Merge branch 'main' into afromher/recursive_projectors
Diffstat (limited to 'compiler/InterpreterStatements.ml')
-rw-r--r-- | compiler/InterpreterStatements.ml | 1450 |
1 files changed, 730 insertions, 720 deletions
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 9ad6487b..c6a65757 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -19,74 +19,68 @@ module S = SynthesizeSymbolic let log = L.statements_log (** Drop a value at a given place - TODO: factorize this with [assign_to_place] *) -let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun = - fun cf ctx -> +let drop_value (config : config) (span : Meta.span) (p : place) : cm_fun = + fun ctx -> log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Note that we use [Write], not [Move]: we allow to drop values *below* borrows *) let access = Write in (* First make sure we can access the place, by ending loans or expanding * symbolic values along the path, for instance *) - let cc = update_ctx_along_read_place config meta access p in + let ctx, cc = update_ctx_along_read_place config span access p ctx in (* Prepare the place (by ending the outer loans *at* the place). *) - let cc = comp cc (prepare_lplace config meta p) in + let v, ctx, cc = comp2 cc (prepare_lplace config span p ctx) in (* Replace the value with {!Bottom} *) - let replace cf (v : typed_value) ctx = + let ctx = (* Move the value at destination (that we will overwrite) to a dummy variable * to preserve the borrows it may contain *) - let mv = InterpreterPaths.read_place meta access p ctx in + let mv = InterpreterPaths.read_place span access p ctx in let dummy_id = fresh_dummy_var_id () in let ctx = ctx_push_dummy_var ctx dummy_id mv in (* Update the destination to ⊥ *) let nv = { v with value = VBottom } in - let ctx = write_place meta access p nv ctx in + let ctx = write_place span access p nv ctx in log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - cf ctx + ^ eval_ctx_to_string ~span:(Some span) ctx)); + ctx in (* Compose and apply *) - comp cc replace cf ctx + (ctx, cc) (** Push a dummy variable to the environment *) -let push_dummy_var (vid : DummyVarId.id) (v : typed_value) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_dummy_var ctx vid v in - cf ctx +let push_dummy_var (vid : DummyVarId.id) (v : typed_value) (ctx : eval_ctx) : + eval_ctx = + ctx_push_dummy_var ctx vid v (** Remove a dummy variable from the environment *) -let remove_dummy_var (meta : Meta.meta) (vid : DummyVarId.id) - (cf : typed_value -> m_fun) : m_fun = - fun ctx -> - let ctx, v = ctx_remove_dummy_var meta ctx vid in - cf v ctx +let remove_dummy_var (span : Meta.span) (vid : DummyVarId.id) (ctx : eval_ctx) : + typed_value * eval_ctx = + let ctx, v = ctx_remove_dummy_var span ctx vid in + (v, ctx) (** Push an uninitialized variable to the environment *) -let push_uninitialized_var (meta : Meta.meta) (var : var) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_uninitialized_var meta ctx var in - cf ctx +let push_uninitialized_var (span : Meta.span) (var : var) (ctx : eval_ctx) : + eval_ctx = + ctx_push_uninitialized_var span ctx var (** Push a list of uninitialized variables to the environment *) -let push_uninitialized_vars (meta : Meta.meta) (vars : var list) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_uninitialized_vars meta ctx vars in - cf ctx +let push_uninitialized_vars (span : Meta.span) (vars : var list) + (ctx : eval_ctx) : eval_ctx = + ctx_push_uninitialized_vars span ctx vars (** Push a variable to the environment *) -let push_var (meta : Meta.meta) (var : var) (v : typed_value) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_var meta ctx var v in - cf ctx +let push_var (span : Meta.span) (var : var) (v : typed_value) (ctx : eval_ctx) : + eval_ctx = + ctx_push_var span ctx var v (** Push a list of variables to the environment *) -let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_vars meta ctx vars in - cf ctx +let push_vars (span : Meta.span) (vars : (var * typed_value) list) + (ctx : eval_ctx) : eval_ctx = + ctx_push_vars span ctx vars (** Assign a value to a given place. @@ -95,69 +89,62 @@ let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) : cm_fun = dummy variable and putting in its destination (after having checked that preparing the destination didn't introduce ⊥). *) -let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value) +let assign_to_place (config : config) (span : Meta.span) (rv : typed_value) (p : place) : cm_fun = - fun cf ctx -> + fun ctx -> log#ldebug (lazy ("assign_to_place:" ^ "\n- rv: " - ^ typed_value_to_string ~meta:(Some meta) ctx rv + ^ typed_value_to_string ~span:(Some span) ctx rv ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Initial context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Push the rvalue to a dummy variable, for bookkeeping *) let rvalue_vid = fresh_dummy_var_id () in - let cc = push_dummy_var rvalue_vid rv in + let ctx = push_dummy_var rvalue_vid rv ctx in (* Prepare the destination *) - let cc = comp cc (prepare_lplace config meta p) in + let _, ctx, cc = prepare_lplace config span p ctx in (* Retrieve the rvalue from the dummy variable *) - let cc = comp cc (fun cf _lv -> remove_dummy_var meta rvalue_vid cf) in + let rv, ctx = remove_dummy_var span rvalue_vid ctx in + (* Move the value at destination (that we will overwrite) to a dummy variable + to preserve the borrows *) + let mv = InterpreterPaths.read_place span Write p ctx in + let dest_vid = fresh_dummy_var_id () in + let ctx = ctx_push_dummy_var ctx dest_vid mv in + (* Write to the destination *) + (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) + exec_assert __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions rv)) + span "The value to move contains bottom"; (* Update the destination *) - let move_dest cf (rv : typed_value) : m_fun = - fun ctx -> - (* Move the value at destination (that we will overwrite) to a dummy variable - * to preserve the borrows *) - let mv = InterpreterPaths.read_place meta Write p ctx in - let dest_vid = fresh_dummy_var_id () in - let ctx = ctx_push_dummy_var ctx dest_vid mv in - (* Write to the destination *) - (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) - exec_assert __FILE__ __LINE__ - (not (bottom_in_value ctx.ended_regions rv)) - meta "The value to move contains bottom"; - (* Update the destination *) - let ctx = write_place meta Write p rv ctx in - (* Debug *) - log#ldebug - (lazy - ("assign_to_place:" ^ "\n- rv: " - ^ typed_value_to_string ~meta:(Some meta) ctx rv - ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - (* Continue *) - cf ctx - in - (* Compose and apply *) - comp cc move_dest cf ctx + let ctx = write_place span Write p rv ctx in + (* Debug *) + log#ldebug + (lazy + ("assign_to_place:" ^ "\n- rv: " + ^ typed_value_to_string ~span:(Some span) ctx rv + ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n" + ^ eval_ctx_to_string ~span:(Some span) ctx)); + (* Return *) + (ctx, cc) (** Evaluate an assertion, when the scrutinee is not symbolic *) -let eval_assertion_concrete (config : config) (meta : Meta.meta) +let eval_assertion_concrete (config : config) (span : Meta.span) (assertion : assertion) : st_cm_fun = - fun cf ctx -> + fun ctx -> (* There won't be any symbolic expansions: fully evaluate the operand *) - let eval_op = eval_operand config meta assertion.cond in - let eval_assert cf (v : typed_value) : m_fun = - fun ctx -> + let v, ctx, eval_op = eval_operand config span assertion.cond ctx in + let st = match v.value with | VLiteral (VBool b) -> (* Branch *) - if b = assertion.expected then cf Unit ctx else cf Panic ctx + if b = assertion.expected then Unit else Panic | _ -> - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span ("Expected a boolean, got: " - ^ typed_value_to_string ~meta:(Some meta) ctx v) + ^ typed_value_to_string ~span:(Some span) ctx v) in (* Compose and apply *) - comp eval_op eval_assert cf ctx + ((ctx, st), eval_op) (** Evaluates an assertion. @@ -165,15 +152,14 @@ let eval_assertion_concrete (config : config) (meta : Meta.meta) a call to [assert ...] then continue in the success branch (and thus expand the boolean to [true]). *) -let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) +let eval_assertion (config : config) (span : Meta.span) (assertion : assertion) : st_cm_fun = - fun cf ctx -> + fun ctx -> (* Evaluate the operand *) - let eval_op = eval_operand config meta assertion.cond in + let v, ctx, cf_eval_op = eval_operand config span assertion.cond ctx in (* Evaluate the assertion *) - let eval_assert cf (v : typed_value) : m_fun = - fun ctx -> - sanity_check __FILE__ __LINE__ (v.ty = TLiteral TBool) meta; + sanity_check __FILE__ __LINE__ (v.ty = TLiteral TBool) span; + let st, cf_eval_assert = (* We make a choice here: we could completely decouple the concrete and * symbolic executions here but choose not to. In the case where we * know the concrete value of the boolean we test, we use this value @@ -182,29 +168,27 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) match v.value with | VLiteral (VBool _) -> (* Delegate to the concrete evaluation function *) - eval_assertion_concrete config meta assertion cf ctx + eval_assertion_concrete config span assertion ctx | VSymbolic sv -> - sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; - sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral TBool) meta; + sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) span; + sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral TBool) span; (* We continue the execution as if the test had succeeded, and thus * perform the symbolic expansion: sv ~~> true. * We will of course synthesize an assertion in the generated code * (see below). *) let ctx = - apply_symbolic_expansion_non_borrow config meta sv - (SeLiteral (VBool true)) ctx + apply_symbolic_expansion_non_borrow config span sv ctx + (SeLiteral (VBool true)) in - (* Continue *) - let expr = cf Unit ctx in (* Add the synthesized assertion *) - S.synthesize_assertion ctx v expr + ((ctx, Unit), S.synthesize_assertion ctx v) | _ -> - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span ("Expected a boolean, got: " - ^ typed_value_to_string ~meta:(Some meta) ctx v) + ^ typed_value_to_string ~span:(Some span) ctx v) in (* Compose and apply *) - comp eval_op eval_assert cf ctx + (st, cc_comp cf_eval_op cf_eval_assert) (** Updates the discriminant of a value at a given place. @@ -217,94 +201,92 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) a variant with all its fields set to {!Bottom}. For instance, something like: [Cons Bottom Bottom]. *) -let set_discriminant (config : config) (meta : Meta.meta) (p : place) +let set_discriminant (config : config) (span : Meta.span) (p : place) (variant_id : VariantId.id) : st_cm_fun = - fun cf ctx -> + fun ctx -> log#ldebug (lazy ("set_discriminant:" ^ "\n- p: " ^ place_to_string ctx p ^ "\n- variant id: " ^ VariantId.to_string variant_id ^ "\n- initial context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Access the value *) let access = Write in - let cc = update_ctx_along_read_place config meta access p in - let cc = comp cc (prepare_lplace config meta p) in + let ctx, cc = update_ctx_along_read_place config span access p ctx in + let v, ctx, cc = comp2 cc (prepare_lplace config span p ctx) in (* Update the value *) - let update_value cf (v : typed_value) : m_fun = - fun ctx -> - match (v.ty, v.value) with - | TAdt ((TAdtId _ as type_id), generics), VAdt av -> ( - (* There are two situations: - - either the discriminant is already the proper one (in which case we - don't do anything) - - or it is not the proper one, in which case we replace the value with - a variant with all its fields set to {!Bottom} - *) - match av.variant_id with - | None -> - craise __FILE__ __LINE__ meta - "Found a struct value while expected an enum" - | Some variant_id' -> - if variant_id' = variant_id then (* Nothing to do *) - cf Unit ctx - else - (* Replace the value *) - let bottom_v = - match type_id with - | TAdtId def_id -> - compute_expanded_bottom_adt_value meta ctx def_id - (Some variant_id) generics - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - assign_to_place config meta bottom_v p (cf Unit) ctx) - | TAdt ((TAdtId _ as type_id), generics), VBottom -> - let bottom_v = - match type_id with - | TAdtId def_id -> - compute_expanded_bottom_adt_value meta ctx def_id - (Some variant_id) generics - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - assign_to_place config meta bottom_v p (cf Unit) ctx - | _, VSymbolic _ -> - sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; - (* This is a bit annoying: in theory we should expand the symbolic value - * then set the discriminant, because in the case the discriminant is - * exactly the one we set, the fields are left untouched, and in the - * other cases they are set to Bottom. - * For now, we forbid setting the discriminant of a symbolic value: - * setting a discriminant should only be used to initialize a value, - * or reset an already initialized value, really. *) - craise __FILE__ __LINE__ meta "Unexpected value" - | _, (VAdt _ | VBottom) -> - craise __FILE__ __LINE__ meta "Inconsistent state" - | _, (VLiteral _ | VBorrow _ | VLoan _) -> - craise __FILE__ __LINE__ meta "Unexpected value" - in - (* Compose and apply *) - comp cc update_value cf ctx + match (v.ty, v.value) with + | TAdt ((TAdtId _ as type_id), generics), VAdt av -> ( + (* There are two situations: + - either the discriminant is already the proper one (in which case we + don't do anything) + - or it is not the proper one, in which case we replace the value with + a variant with all its fields set to {!Bottom} + *) + match av.variant_id with + | None -> + craise __FILE__ __LINE__ span + "Found a struct value while expecting an enum" + | Some variant_id' -> + if variant_id' = variant_id then (* Nothing to do *) + ((ctx, Unit), cc) + else + (* Replace the value *) + let bottom_v = + match type_id with + | TAdtId def_id -> + compute_expanded_bottom_adt_value span ctx def_id + (Some variant_id) generics + | _ -> craise __FILE__ __LINE__ span "Unreachable" + in + let ctx, cc = + comp cc (assign_to_place config span bottom_v p ctx) + in + ((ctx, Unit), cc)) + | TAdt ((TAdtId _ as type_id), generics), VBottom -> + let bottom_v = + match type_id with + | TAdtId def_id -> + compute_expanded_bottom_adt_value span ctx def_id (Some variant_id) + generics + | _ -> craise __FILE__ __LINE__ span "Unreachable" + in + let ctx, cc = comp cc (assign_to_place config span bottom_v p ctx) in + ((ctx, Unit), cc) + | _, VSymbolic _ -> + sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) span; + (* This is a bit annoying: in theory we should expand the symbolic value + * then set the discriminant, because in the case the discriminant is + * exactly the one we set, the fields are left untouched, and in the + * other cases they are set to Bottom. + * For now, we forbid setting the discriminant of a symbolic value: + * setting a discriminant should only be used to initialize a value, + * or reset an already initialized value, really. *) + craise __FILE__ __LINE__ span "Unexpected value" + | _, (VAdt _ | VBottom) -> craise __FILE__ __LINE__ span "Inconsistent state" + | _, (VLiteral _ | VBorrow _ | VLoan _) -> + craise __FILE__ __LINE__ span "Unexpected value" (** Push a frame delimiter in the context's environment *) let ctx_push_frame (ctx : eval_ctx) : eval_ctx = { ctx with env = EFrame :: ctx.env } (** Push a frame delimiter in the context's environment *) -let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx) +let push_frame (ctx : eval_ctx) : eval_ctx = ctx_push_frame ctx (** Small helper: compute the type of the return value for a specific instantiation of an assumed function. *) -let get_assumed_function_return_type (meta : Meta.meta) (ctx : eval_ctx) +let get_assumed_function_return_type (span : Meta.span) (ctx : eval_ctx) (fid : assumed_fun_id) (generics : generic_args) : ety = - sanity_check __FILE__ __LINE__ (generics.trait_refs = []) meta; + sanity_check __FILE__ __LINE__ (generics.trait_refs = []) span; (* [Box::free] has a special treatment *) match fid with | BoxFree -> - sanity_check __FILE__ __LINE__ (generics.regions = []) meta; - sanity_check __FILE__ __LINE__ (List.length generics.types = 1) meta; - sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; + sanity_check __FILE__ __LINE__ (generics.regions = []) span; + sanity_check __FILE__ __LINE__ (List.length generics.types = 1) span; + sanity_check __FILE__ __LINE__ (generics.const_generics = []) span; mk_unit_ty | _ -> (* Retrieve the function's signature *) @@ -320,28 +302,30 @@ let get_assumed_function_return_type (meta : Meta.meta) (ctx : eval_ctx) Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self sg.output in - AssociatedTypes.ctx_normalize_erase_ty meta ctx ty + AssociatedTypes.ctx_normalize_erase_ty span ctx ty -let move_return_value (config : config) (meta : Meta.meta) - (pop_return_value : bool) (cf : typed_value option -> m_fun) : m_fun = - fun ctx -> +let move_return_value (config : config) (span : Meta.span) + (pop_return_value : bool) (ctx : eval_ctx) : + typed_value option * eval_ctx * (eval_result -> eval_result) = if pop_return_value then let ret_vid = VarId.zero in - let cc = eval_operand config meta (Move (mk_place_from_var_id ret_vid)) in - cc (fun v ctx -> cf (Some v) ctx) ctx - else cf None ctx + let v, ctx, cc = + eval_operand config span (Move (mk_place_from_var_id ret_vid)) ctx + in + (Some v, ctx, cc) + else (None, ctx, fun e -> e) -let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool) - (cf : typed_value option -> m_fun) : m_fun = - fun ctx -> +let pop_frame (config : config) (span : Meta.span) (pop_return_value : bool) + (ctx : eval_ctx) : + typed_value option * eval_ctx * (eval_result -> eval_result) = (* Debug *) - log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~span:(Some span) ctx)); (* List the local variables, but the return variable *) let ret_vid = VarId.zero in let rec list_locals env = match env with - | [] -> craise __FILE__ __LINE__ meta "Inconsistent environment" + | [] -> craise __FILE__ __LINE__ span "Inconsistent environment" | EAbs _ :: env -> list_locals env | EBinding (BDummy _, _) :: env -> list_locals env | EBinding (BVar var, _) :: env -> @@ -358,75 +342,60 @@ let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool) ^ "]")); (* Move the return value out of the return variable *) - let cc = move_return_value config meta pop_return_value in - (* Sanity check *) - let cc = - comp_check_value cc (fun ret_value ctx -> - match ret_value with - | None -> () - | Some ret_value -> - sanity_check __FILE__ __LINE__ - (not (bottom_in_value ctx.ended_regions ret_value)) - meta) + let v, ctx, cc = move_return_value config span pop_return_value ctx in + let _ = + match v with + | None -> () + | Some ret_value -> + sanity_check __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions ret_value)) + span in (* Drop the outer *loans* we find in the local variables *) - let cf_drop_loans_in_locals cf (ret_value : typed_value option) : m_fun = - (* Drop the loans *) - let locals = List.rev locals in - let cf_drop = - List.fold_left - (fun cf lid -> - drop_outer_loans_at_lplace config meta (mk_place_from_var_id lid) cf) - (cf ret_value) locals - in - (* Apply *) - cf_drop + let ctx, cc = + comp cc + ((* Drop the loans *) + let locals = List.rev locals in + fold_left_apply_continuation + (fun lid ctx -> + drop_outer_loans_at_lplace config span (mk_place_from_var_id lid) ctx) + locals ctx) in - let cc = comp cc cf_drop_loans_in_locals in (* Debug *) - let cc = - comp_check_value cc (fun _ ctx -> - log#ldebug - (lazy - ("pop_frame: after dropping outer loans in local variables:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx))) - in + log#ldebug + (lazy + ("pop_frame: after dropping outer loans in local variables:\n" + ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Pop the frame - we remove the [Frame] delimiter, and reintroduce all * the local variables (which may still contain borrow permissions - but * no outer loans) as dummy variables in the caller frame *) let rec pop env = match env with - | [] -> craise __FILE__ __LINE__ meta "Inconsistent environment" + | [] -> craise __FILE__ __LINE__ span "Inconsistent environment" | EAbs abs :: env -> EAbs abs :: pop env | EBinding (_, v) :: env -> let vid = fresh_dummy_var_id () in EBinding (BDummy vid, v) :: pop env | EFrame :: env -> (* Stop here *) env in - let cf_pop cf (ret_value : typed_value option) : m_fun = - fun ctx -> - let env = pop ctx.env in - let ctx = { ctx with env } in - cf ret_value ctx - in - (* Compose and apply *) - comp cc cf_pop cf ctx + let env = pop ctx.env in + let ctx = { ctx with env } in + (* Return *) + (v, ctx, cc) (** Pop the current frame and assign the returned value to its destination. *) -let pop_frame_assign (config : config) (meta : Meta.meta) (dest : place) : +let pop_frame_assign (config : config) (span : Meta.span) (dest : place) : cm_fun = - let cf_pop = pop_frame config meta true in - let cf_assign cf ret_value : m_fun = - assign_to_place config meta (Option.get ret_value) dest cf - in - comp cf_pop cf_assign + fun ctx -> + let v, ctx, cc = pop_frame config span true ctx in + comp cc (assign_to_place config span (Option.get v) dest ctx) (** Auxiliary function - see {!eval_assumed_function_call} *) -let eval_box_new_concrete (config : config) (meta : Meta.meta) +let eval_box_new_concrete (config : config) (span : Meta.span) (generics : generic_args) : cm_fun = - fun cf ctx -> + fun ctx -> (* Check and retrieve the arguments *) match (generics.regions, generics.types, generics.const_generics, ctx.env) @@ -440,34 +409,26 @@ let eval_box_new_concrete (config : config) (meta : Meta.meta) (* Required type checking *) cassert __FILE__ __LINE__ (input_value.ty = boxed_ty) - meta "The input given to Box::new doesn't have the proper type"; + span "The input given to Box::new doesn't have the proper type"; (* Move the input value *) - let cf_move = - eval_operand config meta (Move (mk_place_from_var_id input_var.index)) + let v, ctx, cc = + eval_operand config span + (Move (mk_place_from_var_id input_var.index)) + ctx in (* Create the new box *) - let cf_create cf (moved_input_value : typed_value) : m_fun = - (* Create the box value *) - let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in - let box_ty = TAdt (TAssumed TBox, generics) in - let box_v = - VAdt { variant_id = None; field_values = [ moved_input_value ] } - in - let box_v = mk_typed_value meta box_ty box_v in + (* Create the box value *) + let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in + let box_ty = TAdt (TAssumed TBox, generics) in + let box_v = VAdt { variant_id = None; field_values = [ v ] } in + let box_v = mk_typed_value span box_ty box_v in - (* Move this value to the return variable *) - let dest = mk_place_from_var_id VarId.zero in - let cf_assign = assign_to_place config meta box_v dest in - - (* Continue *) - cf_assign cf - in - - (* Compose and apply *) - comp cf_move cf_create cf ctx - | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" + (* Move this value to the return variable *) + let dest = mk_place_from_var_id VarId.zero in + comp cc (assign_to_place config span box_v dest ctx) + | _ -> craise __FILE__ __LINE__ span "Inconsistent state" (** Auxiliary function - see {!eval_assumed_function_call}. @@ -488,43 +449,41 @@ let eval_box_new_concrete (config : config) (meta : Meta.meta) It thus updates the box value (by calling {!drop_value}) and updates the destination (by setting it to [()]). *) -let eval_box_free (config : config) (meta : Meta.meta) (generics : generic_args) +let eval_box_free (config : config) (span : Meta.span) (generics : generic_args) (args : operand list) (dest : place) : cm_fun = - fun cf ctx -> + fun ctx -> match (generics.regions, generics.types, generics.const_generics, args) with | [], [ boxed_ty ], [], [ Move input_box_place ] -> (* Required type checking *) let input_box = - InterpreterPaths.read_place meta Write input_box_place ctx + InterpreterPaths.read_place span Write input_box_place ctx in (let input_ty = ty_get_box input_box.ty in sanity_check __FILE__ __LINE__ (input_ty = boxed_ty)) - meta; + span; (* Drop the value *) - let cc = drop_value config meta input_box_place in + let ctx, cc = drop_value config span input_box_place ctx in (* Update the destination by setting it to [()] *) - let cc = comp cc (assign_to_place config meta mk_unit_value dest) in - - (* Continue *) - cc cf ctx - | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" + comp cc (assign_to_place config span mk_unit_value dest ctx) + | _ -> craise __FILE__ __LINE__ span "Inconsistent state" (** Evaluate a non-local function call in concrete mode *) -let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta) +let eval_assumed_function_call_concrete (config : config) (span : Meta.span) (fid : assumed_fun_id) (call : call) : cm_fun = + fun ctx -> let args = call.args in let dest = call.dest in match call.func with | FnOpMove _ -> (* Closure case: TODO *) - craise __FILE__ __LINE__ meta "Closures are not supported yet" + craise __FILE__ __LINE__ span "Closures are not supported yet" | FnOpRegular func -> ( let generics = func.generics in (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) - sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; + sanity_check __FILE__ __LINE__ (generics.const_generics = []) span; (* There are two cases (and this is extremely annoying): - the function is not box_free - the function is box_free @@ -533,12 +492,12 @@ let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta) match fid with | BoxFree -> (* Degenerate case: box_free *) - eval_box_free config meta generics args dest + eval_box_free config span generics args dest ctx | _ -> (* "Normal" case: not box_free *) (* Evaluate the operands *) (* let ctx, args_vl = eval_operands config ctx args in *) - let cf_eval_ops = eval_operands config meta args in + let args_vl, ctx, cc = eval_operands config span args ctx in (* Evaluate the call * @@ -547,53 +506,42 @@ let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta) * below, without having to introduce an intermediary function call, * but it made it less clear where the computed values came from, * so we reversed the modifications. *) - let cf_eval_call cf (args_vl : typed_value list) : m_fun = - fun ctx -> - (* Push the stack frame: we initialize the frame with the return variable, - and one variable per input argument *) - let cc = push_frame in - - (* Create and push the return variable *) - let ret_vid = VarId.zero in - let ret_ty = - get_assumed_function_return_type meta ctx fid generics - in - let ret_var = mk_var ret_vid (Some "@return") ret_ty in - let cc = comp cc (push_uninitialized_var meta ret_var) in - - (* Create and push the input variables *) - let input_vars = - VarId.mapi_from1 - (fun id (v : typed_value) -> (mk_var id None v.ty, v)) - args_vl - in - let cc = comp cc (push_vars meta input_vars) in - - (* "Execute" the function body. As the functions are assumed, here we call - * custom functions to perform the proper manipulations: we don't have - * access to a body. *) - let cf_eval_body : cm_fun = - match fid with - | BoxNew -> eval_box_new_concrete config meta generics - | BoxFree -> - (* Should have been treated above *) - craise __FILE__ __LINE__ meta "Unreachable" - | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared - | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut - -> - craise __FILE__ __LINE__ meta "Unimplemented" - in - - let cc = comp cc cf_eval_body in - - (* Pop the frame *) - let cc = comp cc (pop_frame_assign config meta dest) in - - (* Continue *) - cc cf ctx + (* Push the stack frame: we initialize the frame with the return variable, + and one variable per input argument *) + let ctx = push_frame ctx in + + (* Create and push the return variable *) + let ret_vid = VarId.zero in + let ret_ty = get_assumed_function_return_type span ctx fid generics in + let ret_var = mk_var ret_vid (Some "@return") ret_ty in + let ctx = push_uninitialized_var span ret_var ctx in + + (* Create and push the input variables *) + let input_vars = + VarId.mapi_from1 + (fun id (v : typed_value) -> (mk_var id None v.ty, v)) + args_vl in - (* Compose and apply *) - comp cf_eval_ops cf_eval_call) + let ctx = push_vars span input_vars ctx in + + (* "Execute" the function body. As the functions are assumed, here we call + * custom functions to perform the proper manipulations: we don't have + * access to a body. *) + let ctx, cf_eval_body = + match fid with + | BoxNew -> eval_box_new_concrete config span generics ctx + | BoxFree -> + (* Should have been treated above *) + craise __FILE__ __LINE__ span "Unreachable" + | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared + | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut + -> + craise __FILE__ __LINE__ span "Unimplemented" + in + let cc = cc_comp cc cf_eval_body in + + (* Pop the frame *) + comp cc (pop_frame_assign config span dest ctx)) (** Helper @@ -750,7 +698,7 @@ let create_push_abstractions_from_abs_region_groups which means that whenever we call a provided trait method, we do not refer to a trait clause but directly to the method provided in the trait declaration. *) -let eval_transparent_function_call_symbolic_inst (meta : Meta.meta) +let eval_transparent_function_call_symbolic_inst (span : Meta.span) (call : call) (ctx : eval_ctx) : fun_id_or_trait_method_ref * generic_args @@ -761,7 +709,7 @@ let eval_transparent_function_call_symbolic_inst (meta : Meta.meta) match call.func with | FnOpMove _ -> (* Closure case: TODO *) - craise __FILE__ __LINE__ meta "Closures are not supported yet" + craise __FILE__ __LINE__ span "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular fid) -> @@ -779,13 +727,13 @@ let eval_transparent_function_call_symbolic_inst (meta : Meta.meta) ctx.fun_ctx.regions_hierarchies in let inst_sg = - instantiate_fun_sig meta ctx func.generics tr_self def.signature + instantiate_fun_sig span ctx func.generics tr_self def.signature regions_hierarchy in (func.func, func.generics, None, def, regions_hierarchy, inst_sg) | FunId (FAssumed _) -> (* Unreachable: must be a transparent function *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" | TraitMethod (trait_ref, method_name, _) -> ( log#ldebug (lazy @@ -826,7 +774,7 @@ let eval_transparent_function_call_symbolic_inst (meta : Meta.meta) ctx.fun_ctx.regions_hierarchies in let inst_sg = - instantiate_fun_sig meta ctx generics tr_self + instantiate_fun_sig span ctx generics tr_self method_def.signature regions_hierarchy in (* Also update the function identifier: we want to forget @@ -847,7 +795,7 @@ let eval_transparent_function_call_symbolic_inst (meta : Meta.meta) (remember: for now, we forbid overriding provided methods) *) cassert __FILE__ __LINE__ (trait_impl.provided_methods = []) - meta "Overriding provided methods is currently forbidden"; + span "Overriding provided methods is currently forbidden"; let trait_decl = ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id @@ -894,7 +842,7 @@ let eval_transparent_function_call_symbolic_inst (meta : Meta.meta) in let tr_self = TraitRef trait_ref in let inst_sg = - instantiate_fun_sig meta ctx all_generics tr_self + instantiate_fun_sig span ctx all_generics tr_self method_def.signature regions_hierarchy in ( func.func, @@ -936,7 +884,7 @@ let eval_transparent_function_call_symbolic_inst (meta : Meta.meta) in let tr_self = TraitRef trait_ref in let inst_sg = - instantiate_fun_sig meta ctx generics tr_self + instantiate_fun_sig span ctx generics tr_self method_def.signature regions_hierarchy in ( func.func, @@ -947,28 +895,27 @@ let eval_transparent_function_call_symbolic_inst (meta : Meta.meta) inst_sg ))) (** Evaluate a statement *) -let rec eval_statement (config : config) (st : statement) : st_cm_fun = - fun cf ctx -> +let rec eval_statement (config : config) (st : statement) : stl_cm_fun = + fun ctx -> (* Debugging *) log#ldebug (lazy ("\n**About to evaluate statement**: [\n" ^ statement_to_string_with_tab ctx st ^ "\n]\n\n**Context**:\n" - ^ eval_ctx_to_string ~meta:(Some st.meta) ctx + ^ eval_ctx_to_string ~span:(Some st.span) ctx ^ "\n\n")); (* Take a snapshot of the current context for the purpose of generating pretty names *) - let cc = S.cf_save_snapshot in + let cc = S.save_snapshot ctx in (* Expand the symbolic values if necessary - we need to do that before - * checking the invariants *) - let cc = comp cc (greedy_expand_symbolic_values config st.meta) in + checking the invariants *) + let ctx, cc = comp cc (greedy_expand_symbolic_values config st.span ctx) in (* Sanity check *) - let cc = comp cc (Invariants.cf_check_invariants st.meta) in + Invariants.check_invariants st.span ctx; (* Evaluate *) - let cf_eval_st cf : m_fun = - fun ctx -> + let stl, cf_eval_st = log#ldebug (lazy ("\neval_statement: cf_eval_st: statement:\n" @@ -980,96 +927,118 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = match rvalue with | Global (gid, generics) -> (* Evaluate the global *) - eval_global config p gid generics cf ctx + eval_global config st.span p gid generics ctx | _ -> (* Evaluate the rvalue *) - let cf_eval_rvalue = eval_rvalue_not_global config st.meta rvalue in + let res, ctx, cc = + eval_rvalue_not_global config st.span rvalue ctx + in (* Assign *) - let cf_assign cf (res : (typed_value, eval_error) result) ctx = - log#ldebug - (lazy - ("about to assign to place: " ^ place_to_string ctx p - ^ "\n- Context:\n" - ^ eval_ctx_to_string ~meta:(Some st.meta) ctx)); + log#ldebug + (lazy + ("about to assign to place: " ^ place_to_string ctx p + ^ "\n- Context:\n" + ^ eval_ctx_to_string ~span:(Some st.span) ctx)); + let (ctx, res), cf_assign = match res with - | Error EPanic -> cf Panic ctx - | Ok rv -> ( - let expr = - assign_to_place config st.meta rv p (cf Unit) ctx - in - (* Update the synthesized AST - here we store meta-information. + | Error EPanic -> ((ctx, Panic), fun e -> e) + | Ok rv -> + (* Update the synthesized AST - here we store additional span-information. * We do it only in specific cases (it is not always useful, and * also it can lead to issues - for instance, if we borrow a * reserved borrow, we later can't translate it to pure values...) *) - match rvalue with - | Global _ -> craise __FILE__ __LINE__ st.meta "Unreachable" - | Use _ - | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) - | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> - let rp = rvalue_get_place rvalue in - let rp = - match rp with - | Some rp -> Some (S.mk_mplace st.meta rp ctx) - | None -> None - in - S.synthesize_assignment ctx - (S.mk_mplace st.meta p ctx) - rv rp expr) + let cc = + match rvalue with + | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable" + | Use _ + | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) + | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> + let rp = rvalue_get_place rvalue in + let rp = + match rp with + | Some rp -> Some (S.mk_mplace st.span rp ctx) + | None -> None + in + S.synthesize_assignment ctx + (S.mk_mplace st.span p ctx) + rv rp + in + let ctx, cc = + comp cc (assign_to_place config st.span rv p ctx) + in + ((ctx, Unit), cc) in - + let cc = cc_comp cc cf_assign in (* Compose and apply *) - comp cf_eval_rvalue cf_assign cf ctx) - | FakeRead p -> eval_fake_read config st.meta p (cf Unit) ctx + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc)) + | FakeRead p -> + let ctx, cc = eval_fake_read config st.span p ctx in + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.span cc) | SetDiscriminant (p, variant_id) -> - set_discriminant config st.meta p variant_id cf ctx - | Drop p -> drop_value config st.meta p (cf Unit) ctx - | Assert assertion -> eval_assertion config st.meta assertion cf ctx - | Call call -> eval_function_call config st.meta call cf ctx - | Panic -> cf Panic ctx - | Return -> cf Return ctx - | Break i -> cf (Break i) ctx - | Continue i -> cf (Continue i) ctx - | Nop -> cf Unit ctx + let (ctx, res), cc = set_discriminant config st.span p variant_id ctx in + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc) + | Drop p -> + let ctx, cc = drop_value config st.span p ctx in + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.span cc) + | Assert assertion -> + let (ctx, res), cc = eval_assertion config st.span assertion ctx in + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc) + | Call call -> eval_function_call config st.span call ctx + | Panic -> ([ (ctx, Panic) ], cc_singleton __FILE__ __LINE__ st.span cc) + | Return -> ([ (ctx, Return) ], cc_singleton __FILE__ __LINE__ st.span cc) + | Break i -> ([ (ctx, Break i) ], cc_singleton __FILE__ __LINE__ st.span cc) + | Continue i -> + ([ (ctx, Continue i) ], cc_singleton __FILE__ __LINE__ st.span cc) + | Nop -> ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.span cc) | Sequence (st1, st2) -> (* Evaluate the first statement *) - let cf_st1 = eval_statement config st1 in - (* Evaluate the sequence *) - let cf_st2 cf res = - match res with - (* Evaluation successful: evaluate the second statement *) - | Unit -> eval_statement config st2 cf - (* Control-flow break: transmit. We enumerate the cases on purpose *) - | Panic | Break _ | Continue _ | Return | LoopReturn _ - | EndEnterLoop _ | EndContinue _ -> - cf res + let ctx_resl, cf_st1 = eval_statement config st1 ctx in + (* Evaluate the sequence (evaluate the second statement if the first + statement successfully evaluated, otherwise transfmit the control-flow + break) *) + let ctx_res_cfl = + List.map + (fun (ctx, res) -> + match res with + (* Evaluation successful: evaluate the second statement *) + | Unit -> eval_statement config st2 ctx + (* Control-flow break: transmit. We enumerate the cases on purpose *) + | Panic | Break _ | Continue _ | Return | LoopReturn _ + | EndEnterLoop _ | EndContinue _ -> + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc)) + ctx_resl + in + (* Put everything together: + - we return the flattened list of contexts and results + - we need to build the continuation which will build the whole + expression from the continuations for the individual branches + *) + let ctx_resl, cf_st2 = + comp_seqs __FILE__ __LINE__ st.span ctx_res_cfl in - (* Compose and apply *) - comp cf_st1 cf_st2 cf ctx + (ctx_resl, cc_comp cf_st1 cf_st2) | Loop loop_body -> - InterpreterLoops.eval_loop config st.meta - (eval_statement config loop_body) - cf ctx - | Switch switch -> eval_switch config st.meta switch cf ctx + let eval_loop_body = eval_statement config loop_body in + InterpreterLoops.eval_loop config st.span eval_loop_body ctx + | Switch switch -> eval_switch config st.span switch ctx in (* Compose and apply *) - comp cc cf_eval_st cf ctx + (stl, cc_comp cc cf_eval_st) -and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) - (generics : generic_args) : st_cm_fun = - fun cf ctx -> +and eval_global (config : config) (span : Meta.span) (dest : place) + (gid : GlobalDeclId.id) (generics : generic_args) : stl_cm_fun = + fun ctx -> let global = ctx_lookup_global_decl ctx gid in match config.mode with | ConcreteMode -> (* Treat the evaluation of the global as a call to the global body *) let func = { func = FunId (FRegular global.body); generics } in let call = { func = FnOpRegular func; args = []; dest } in - (eval_transparent_function_call_concrete config global.item_meta.meta - global.body call) - cf ctx - | SymbolicMode -> + eval_transparent_function_call_concrete config span global.body call ctx + | SymbolicMode -> ( (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *) - cassert __FILE__ __LINE__ (ty_no_regions global.ty) global.item_meta.meta + cassert __FILE__ __LINE__ (ty_no_regions global.ty) span "Const globals should not contain regions"; (* Instantiate the type *) (* There shouldn't be any reference to Self *) @@ -1082,19 +1051,24 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self global.ty in - let sval = mk_fresh_symbolic_value global.item_meta.meta ty in - let cc = - assign_to_place config global.item_meta.meta + let sval = mk_fresh_symbolic_value span ty in + let ctx, cc = + assign_to_place config span (mk_typed_value_from_symbolic_value sval) - dest + dest ctx in - let e = cc (cf Unit) ctx in - S.synthesize_global_eval gid generics sval e + ( [ (ctx, Unit) ], + fun el -> + match el with + | Some [ e ] -> + (cc_comp (S.synthesize_global_eval gid generics sval) cc) (Some e) + | Some _ -> internal_error __FILE__ __LINE__ span + | _ -> None )) (** Evaluate a switch *) -and eval_switch (config : config) (meta : Meta.meta) (switch : switch) : - st_cm_fun = - fun cf ctx -> +and eval_switch (config : config) (span : Meta.span) (switch : switch) : + stl_cm_fun = + fun ctx -> (* We evaluate the operand in two steps: * first we prepare it, then we check if its value is concrete or * symbolic. If it is concrete, we can then evaluate the operand @@ -1104,286 +1078,317 @@ and eval_switch (config : config) (meta : Meta.meta) (switch : switch) : * (and would thus floating in thin air...)! * *) (* Match on the targets *) - let cf_match : st_cm_fun = - fun cf ctx -> - match switch with - | If (op, st1, st2) -> - (* Evaluate the operand *) - let cf_eval_op = eval_operand config meta op in - (* Switch on the value *) - let cf_if (cf : st_m_fun) (op_v : typed_value) : m_fun = - fun ctx -> - match op_v.value with - | VLiteral (VBool b) -> - (* Evaluate the if and the branch body *) - let cf_branch cf : m_fun = - (* Branch *) - if b then eval_statement config st1 cf - else eval_statement config st2 cf - in - (* Compose the continuations *) - cf_branch cf ctx - | VSymbolic sv -> - (* Expand the symbolic boolean, and continue by evaluating - * the branches *) - let cf_true : st_cm_fun = eval_statement config st1 in - let cf_false : st_cm_fun = eval_statement config st2 in - expand_symbolic_bool config meta sv - (S.mk_opt_place_from_op meta op ctx) - cf_true cf_false cf ctx - | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" - in - (* Compose *) - comp cf_eval_op cf_if cf ctx - | SwitchInt (op, int_ty, stgts, otherwise) -> - (* Evaluate the operand *) - let cf_eval_op = eval_operand config meta op in - (* Switch on the value *) - let cf_switch (cf : st_m_fun) (op_v : typed_value) : m_fun = - fun ctx -> - match op_v.value with - | VLiteral (VScalar sv) -> - (* Evaluate the branch *) - let cf_eval_branch cf = - (* Sanity check *) - sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta; - (* Find the branch *) - match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with - | None -> eval_statement config otherwise cf - | Some (_, tgt) -> eval_statement config tgt cf - in - (* Compose *) - cf_eval_branch cf ctx - | VSymbolic sv -> - (* Expand the symbolic value and continue by evaluating the - * proper branches *) - let stgts = - List.map - (fun (cv, tgt_st) -> (cv, eval_statement config tgt_st)) - stgts - in - (* Several branches may be grouped together: every branch is described - * by a pair (list of values, branch expression). - * In order to do a symbolic evaluation, we make this "flat" by - * de-grouping the branches. *) - let stgts = - List.concat - (List.map - (fun (vl, st) -> List.map (fun v -> (v, st)) vl) - stgts) - in - (* Translate the otherwise branch *) - let otherwise = eval_statement config otherwise in - (* Expand and continue *) - expand_symbolic_int config meta sv - (S.mk_opt_place_from_op meta op ctx) - int_ty stgts otherwise cf ctx - | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" - in - (* Compose *) - comp cf_eval_op cf_switch cf ctx - | Match (p, stgts, otherwise) -> - (* Access the place *) - let access = Read in - let expand_prim_copy = false in - let cf_read_p cf : m_fun = - access_rplace_reorganize_and_read config meta expand_prim_copy access - p cf - in - (* Match on the value *) - let cf_match (cf : st_m_fun) (p_v : typed_value) : m_fun = - fun ctx -> - (* The value may be shared: we need to ignore the shared loans - to read the value itself *) - let p_v = value_strip_shared_loans p_v in - (* Match *) - match p_v.value with - | VAdt adt -> ( - (* Evaluate the discriminant *) - let dv = Option.get adt.variant_id in - (* Find the branch, evaluate and continue *) - match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with - | None -> ( - match otherwise with - | None -> craise __FILE__ __LINE__ meta "No otherwise branch" - | Some otherwise -> eval_statement config otherwise cf ctx) - | Some (_, tgt) -> eval_statement config tgt cf ctx) - | VSymbolic sv -> - (* Expand the symbolic value - may lead to branching *) - let cf_expand = - expand_symbolic_adt config meta sv - (Some (S.mk_mplace meta p ctx)) - in - (* Re-evaluate the switch - the value is not symbolic anymore, - which means we will go to the other branch *) - cf_expand (eval_switch config meta switch) cf ctx - | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" - in - (* Compose *) - comp cf_read_p cf_match cf ctx - in - (* Compose the continuations *) - cf_match cf ctx + match switch with + | If (op, st1, st2) -> + (* Evaluate the operand *) + let op_v, ctx, cf_eval_op = eval_operand config span op ctx in + (* Switch on the value *) + let ctx_resl, cf_if = + match op_v.value with + | VLiteral (VBool b) -> + (* Branch *) + if b then eval_statement config st1 ctx + else eval_statement config st2 ctx + | VSymbolic sv -> + (* Expand the symbolic boolean, and continue by evaluating + the branches *) + let (ctx_true, ctx_false), cf_bool = + expand_symbolic_bool config span sv + (S.mk_opt_place_from_op span op ctx) + ctx + in + let resl_true = eval_statement config st1 ctx_true in + let resl_false = eval_statement config st2 ctx_false in + let ctx_resl, cf_branches = + comp_seqs __FILE__ __LINE__ span [ resl_true; resl_false ] + in + let cc el = + match cf_branches el with + | None -> None + | Some [ e_true; e_false ] -> cf_bool (Some (e_true, e_false)) + | _ -> internal_error __FILE__ __LINE__ span + in + (ctx_resl, cc) + | _ -> craise __FILE__ __LINE__ span "Inconsistent state" + in + (* Compose *) + (ctx_resl, cc_comp cf_eval_op cf_if) + | SwitchInt (op, int_ty, stgts, otherwise) -> + (* Evaluate the operand *) + let op_v, ctx, cf_eval_op = eval_operand config span op ctx in + (* Switch on the value *) + let ctx_resl, cf_switch = + match op_v.value with + | VLiteral (VScalar sv) -> ( + (* Sanity check *) + sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) span; + (* Find the branch *) + match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with + | None -> eval_statement config otherwise ctx + | Some (_, tgt) -> eval_statement config tgt ctx) + | VSymbolic sv -> + (* Several branches may be grouped together: every branch is described + by a pair (list of values, branch expression). + In order to do a symbolic evaluation, we make this "flat" by + de-grouping the branches. *) + let values, branches = + List.split + (List.concat + (List.map + (fun (vl, st) -> List.map (fun v -> (v, st)) vl) + stgts)) + in + (* Expand the symbolic value *) + let (ctx_branches, ctx_otherwise), cf_int = + expand_symbolic_int config span sv + (S.mk_opt_place_from_op span op ctx) + int_ty values ctx + in + (* Evaluate the branches: first the "regular" branches *) + let resl_branches = + List.map + (fun (ctx, branch) -> eval_statement config branch ctx) + (List.combine ctx_branches branches) + in + (* Then evaluate the "otherwise" branch *) + let resl_otherwise = + eval_statement config otherwise ctx_otherwise + in + (* Compose the continuations *) + let resl, cf = + comp_seqs __FILE__ __LINE__ span + (resl_branches @ [ resl_otherwise ]) + in + let cc el = + match el with + | None -> None + | Some el -> + let el, e_otherwise = Collections.List.pop_last el in + cf_int (Some (el, e_otherwise)) + in + (resl, cc_comp cc cf) + | _ -> craise __FILE__ __LINE__ span "Inconsistent state" + in + (* Compose *) + (ctx_resl, cc_comp cf_eval_op cf_switch) + | Match (p, stgts, otherwise) -> + (* Access the place *) + let access = Read in + let expand_prim_copy = false in + let p_v, ctx, cf_read_p = + access_rplace_reorganize_and_read config span expand_prim_copy access p + ctx + in + (* Match on the value *) + let ctx_resl, cf_match = + (* The value may be shared: we need to ignore the shared loans + to read the value itself *) + let p_v = value_strip_shared_loans p_v in + (* Match *) + match p_v.value with + | VAdt adt -> ( + (* Evaluate the discriminant *) + let dv = Option.get adt.variant_id in + (* Find the branch, evaluate and continue *) + match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with + | None -> ( + match otherwise with + | None -> craise __FILE__ __LINE__ span "No otherwise branch" + | Some otherwise -> eval_statement config otherwise ctx) + | Some (_, tgt) -> eval_statement config tgt ctx) + | VSymbolic sv -> + (* Expand the symbolic value - may lead to branching *) + let ctxl, cf_expand = + expand_symbolic_adt config span sv + (Some (S.mk_mplace span p ctx)) + ctx + in + (* Re-evaluate the switch - the value is not symbolic anymore, + which means we will go to the other branch *) + let resl = + List.map (fun ctx -> (eval_switch config span switch) ctx) ctxl + in + (* Compose the continuations *) + let ctx_resl, cf = comp_seqs __FILE__ __LINE__ span resl in + (ctx_resl, cc_comp cf_expand cf) + | _ -> craise __FILE__ __LINE__ span "Inconsistent state" + in + (* Compose *) + (ctx_resl, cc_comp cf_read_p cf_match) (** Evaluate a function call (auxiliary helper for [eval_statement]) *) -and eval_function_call (config : config) (meta : Meta.meta) (call : call) : - st_cm_fun = +and eval_function_call (config : config) (span : Meta.span) (call : call) : + stl_cm_fun = (* There are several cases: - this is a local function, in which case we execute its body - this is an assumed function, in which case there is a special treatment - this is a trait method *) match config.mode with - | ConcreteMode -> eval_function_call_concrete config meta call - | SymbolicMode -> eval_function_call_symbolic config meta call + | ConcreteMode -> eval_function_call_concrete config span call + | SymbolicMode -> eval_function_call_symbolic config span call -and eval_function_call_concrete (config : config) (meta : Meta.meta) - (call : call) : st_cm_fun = - fun cf ctx -> +and eval_function_call_concrete (config : config) (span : Meta.span) + (call : call) : stl_cm_fun = + fun ctx -> match call.func with - | FnOpMove _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" + | FnOpMove _ -> craise __FILE__ __LINE__ span "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular fid) -> - eval_transparent_function_call_concrete config meta fid call cf ctx - | FunId (FAssumed fid) -> + eval_transparent_function_call_concrete config span fid call ctx + | FunId (FAssumed fid) -> ( (* Continue - note that we do as if the function call has been successful, * by giving {!Unit} to the continuation, because we place us in the case * where we haven't panicked. Of course, the translation needs to take the * panic case into account... *) - eval_assumed_function_call_concrete config meta fid call (cf Unit) ctx - | TraitMethod _ -> craise __FILE__ __LINE__ meta "Unimplemented") - -and eval_function_call_symbolic (config : config) (meta : Meta.meta) - (call : call) : st_cm_fun = + let ctx, cc = + eval_assumed_function_call_concrete config span fid call ctx + in + ( [ (ctx, Unit) ], + fun el -> + match el with + | Some [ e ] -> cc (Some e) + | Some _ -> internal_error __FILE__ __LINE__ span + | _ -> None )) + | TraitMethod _ -> craise __FILE__ __LINE__ span "Unimplemented") + +and eval_function_call_symbolic (config : config) (span : Meta.span) + (call : call) : stl_cm_fun = match call.func with - | FnOpMove _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" + | FnOpMove _ -> craise __FILE__ __LINE__ span "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular _) | TraitMethod _ -> - eval_transparent_function_call_symbolic config meta call + eval_transparent_function_call_symbolic config span call | FunId (FAssumed fid) -> - eval_assumed_function_call_symbolic config meta fid call func) + eval_assumed_function_call_symbolic config span fid call func) (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) -and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta) - (fid : FunDeclId.id) (call : call) : st_cm_fun = +and eval_transparent_function_call_concrete (config : config) (span : Meta.span) + (fid : FunDeclId.id) (call : call) : stl_cm_fun = + fun ctx -> let args = call.args in let dest = call.dest in match call.func with - | FnOpMove _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" + | FnOpMove _ -> craise __FILE__ __LINE__ span "Closures are not supported yet" | FnOpRegular func -> let generics = func.generics in (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) - sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; - fun cf ctx -> - (* Retrieve the (correctly instantiated) body *) - let def = ctx_lookup_fun_decl ctx fid in - (* We can evaluate the function call only if it is not opaque *) - let body = - match def.body with - | None -> - craise __FILE__ __LINE__ meta - ("Can't evaluate a call to an opaque function: " - ^ name_to_string ctx def.name) - | Some body -> body - in - (* TODO: we need to normalize the types if we want to correctly support traits *) - cassert __FILE__ __LINE__ (generics.trait_refs = []) body.meta - "Traits are not supported yet in concrete mode"; - (* There shouldn't be any reference to Self *) - let tr_self = UnknownTrait __FUNCTION__ in - let subst = - Subst.make_subst_from_generics def.signature.generics generics tr_self - in - let locals, body_st = Subst.fun_body_substitute_in_body subst body in - - (* Evaluate the input operands *) - sanity_check __FILE__ __LINE__ - (List.length args = body.arg_count) - body.meta; - let cc = eval_operands config body.meta args in - - (* Push a frame delimiter - we use {!comp_transmit} to transmit the result - * of the operands evaluation from above to the functions afterwards, while - * ignoring it in this function *) - let cc = comp_transmit cc push_frame in - - (* Compute the initial values for the local variables *) - (* 1. Push the return value *) - let ret_var, locals = - match locals with - | ret_ty :: locals -> (ret_ty, locals) - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - let input_locals, locals = - Collections.List.split_at locals body.arg_count - in + sanity_check __FILE__ __LINE__ (generics.const_generics = []) span; + (* Retrieve the (correctly instantiated) body *) + let def = ctx_lookup_fun_decl ctx fid in + (* We can evaluate the function call only if it is not opaque *) + let body = + match def.body with + | None -> + craise __FILE__ __LINE__ span + ("Can't evaluate a call to an opaque function: " + ^ name_to_string ctx def.name) + | Some body -> body + in + (* TODO: we need to normalize the types if we want to correctly support traits *) + cassert __FILE__ __LINE__ (generics.trait_refs = []) body.span + "Traits are not supported yet in concrete mode"; + (* There shouldn't be any reference to Self *) + let tr_self = UnknownTrait __FUNCTION__ in + let subst = + Subst.make_subst_from_generics def.signature.generics generics tr_self + in + let locals, body_st = Subst.fun_body_substitute_in_body subst body in + + (* Evaluate the input operands *) + sanity_check __FILE__ __LINE__ + (List.length args = body.arg_count) + body.span; + let vl, ctx, cc = eval_operands config body.span args ctx in + + (* Push a frame delimiter - we use {!comp_transmit} to transmit the result + * of the operands evaluation from above to the functions afterwards, while + * ignoring it in this function *) + let ctx = push_frame ctx in + + (* Compute the initial values for the local variables *) + (* 1. Push the return value *) + let ret_var, locals = + match locals with + | ret_ty :: locals -> (ret_ty, locals) + | _ -> craise __FILE__ __LINE__ span "Unreachable" + in + let input_locals, locals = + Collections.List.split_at locals body.arg_count + in - let cc = - comp_transmit cc - (push_var meta ret_var (mk_bottom meta ret_var.var_ty)) - in + let ctx = push_var span ret_var (mk_bottom span ret_var.var_ty) ctx in - (* 2. Push the input values *) - let cf_push_inputs cf args = - 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) *) - push_vars meta inputs cf - in - let cc = comp cc cf_push_inputs in - - (* 3. Push the remaining local variables (initialized as {!Bottom}) *) - let cc = comp cc (push_uninitialized_vars meta locals) in - - (* Execute the function body *) - let cc = comp cc (eval_function_body config body_st) in - - (* Pop the stack frame and move the return value to its destination *) - let cf_finish cf res = - match res with - | Panic -> cf Panic - | Return -> - (* Pop the stack frame, retrieve the return value, move it to - * its destination and continue *) - pop_frame_assign config meta dest (cf Unit) - | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ - | EndContinue _ -> - craise __FILE__ __LINE__ meta "Unreachable" - in - let cc = comp cc cf_finish in + (* 2. Push the input values *) + let ctx = + let inputs = List.combine input_locals vl in + (* Note that this function checks that the variables and their values + * have the same type (this is important) *) + push_vars span inputs ctx + in - (* Continue *) - cc cf ctx + (* 3. Push the remaining local variables (initialized as {!Bottom}) *) + let ctx = push_uninitialized_vars span locals ctx in + + (* Execute the function body *) + let ctx_resl, cc = comp cc (eval_function_body config body_st ctx) in + + (* Pop the stack frame and move the return value to its destination *) + let ctx_resl_cfl = + List.map + (fun (ctx, res) -> + match res with + | Panic -> ((ctx, Panic), fun e -> e) + | Return -> + (* Pop the stack frame, retrieve the return value, move it to + its destination and continue *) + let ctx, cf = pop_frame_assign config span dest ctx in + ((ctx, Unit), cf) + | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ + | EndContinue _ -> + craise __FILE__ __LINE__ span "Unreachable") + ctx_resl + in + let ctx_resl, cfl = List.split ctx_resl_cfl in + let cf_pop el = + match el with + | None -> None + | Some el -> + Some + (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el)) + in + (* Continue *) + (ctx_resl, cc_comp cc cf_pop) (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) -and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta) - (call : call) : st_cm_fun = - fun cf ctx -> +and eval_transparent_function_call_symbolic (config : config) (span : Meta.span) + (call : call) : stl_cm_fun = + fun ctx -> let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg = - eval_transparent_function_call_symbolic_inst meta call ctx + eval_transparent_function_call_symbolic_inst span call ctx in (* Sanity check: same number of inputs *) sanity_check __FILE__ __LINE__ (List.length call.args = List.length def.signature.inputs) - def.item_meta.meta; + def.item_meta.span; (* Sanity check: no nested borrows, borrows in ADTs, etc. *) cassert __FILE__ __LINE__ (List.for_all (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty)) (inst_sg.output :: inst_sg.inputs)) - meta "Nested borrows are not supported yet"; + span "Nested borrows are not supported yet"; cassert __FILE__ __LINE__ (List.for_all (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty)) (inst_sg.output :: inst_sg.inputs)) - meta "ADTs containing borrows are not supported yet"; + span "ADTs containing borrows are not supported yet"; (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config def.item_meta.meta func + eval_function_call_symbolic_from_inst_sig config def.item_meta.span func def.signature regions_hierarchy inst_sg generics trait_method_generics - call.args call.dest cf ctx + call.args call.dest ctx (** Evaluate a function call in symbolic mode by using the function signature. @@ -1397,12 +1402,12 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta) trait ref as input. *) and eval_function_call_symbolic_from_inst_sig (config : config) - (meta : Meta.meta) (fid : fun_id_or_trait_method_ref) (sg : fun_sig) + (span : Meta.span) (fid : fun_id_or_trait_method_ref) (sg : fun_sig) (regions_hierarchy : region_var_groups) (inst_sg : inst_fun_sig) (generics : generic_args) (trait_method_generics : (generic_args * trait_instance_id) option) - (args : operand list) (dest : place) : st_cm_fun = - fun cf ctx -> + (args : operand list) (dest : place) : stl_cm_fun = + fun ctx -> log#ldebug (lazy ("eval_function_call_symbolic_from_inst_sig:\n- fid: " @@ -1417,81 +1422,76 @@ and eval_function_call_symbolic_from_inst_sig (config : config) (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.output in - let ret_spc = mk_fresh_symbolic_value meta ret_sv_ty in + let ret_spc = mk_fresh_symbolic_value span ret_sv_ty in let ret_value = mk_typed_value_from_symbolic_value ret_spc in let ret_av regions = mk_aproj_loans_value_from_symbolic_value regions ret_spc in let args_places = - List.map (fun p -> S.mk_opt_place_from_op meta p ctx) args + List.map (fun p -> S.mk_opt_place_from_op span p ctx) args in - let dest_place = Some (S.mk_mplace meta dest ctx) in + let dest_place = Some (S.mk_mplace span dest ctx) in (* Evaluate the input operands *) - let cc = eval_operands config meta args in + let args, ctx, cc = eval_operands config span args ctx in (* Generate the abstractions and insert them in the context *) let abs_ids = List.map (fun rg -> rg.id) inst_sg.regions_hierarchy in - let cf_call cf (args : typed_value list) : m_fun = - fun ctx -> - let args_with_rtypes = List.combine args inst_sg.inputs in - - (* Check the type of the input arguments *) - cassert __FILE__ __LINE__ - (List.for_all - (fun ((arg, rty) : typed_value * rty) -> - arg.ty = Subst.erase_regions rty) - args_with_rtypes) - meta "The input arguments don't have the proper type"; - (* Check that the input arguments don't contain symbolic values that can't - * be fed to functions (i.e., symbolic values output from function return - * values and which contain borrows of borrows can't be used as function - * inputs *) - sanity_check __FILE__ __LINE__ - (List.for_all - (fun arg -> - not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) - args) - meta; - - (* Initialize the abstractions and push them in the context. - * First, we define the function which, given an initialized, empty - * abstraction, computes the avalues which should be inserted inside. - *) - let compute_abs_avalues (abs : abs) (ctx : eval_ctx) : - eval_ctx * typed_avalue list = - (* Project over the input values *) - let ctx, args_projs = - List.fold_left_map - (fun ctx (arg, arg_rty) -> - apply_proj_borrows_on_input_value config meta ctx abs.regions - abs.ancestors_regions arg arg_rty) - ctx args_with_rtypes - in - (* Group the input and output values *) - (ctx, List.append args_projs [ ret_av abs.regions ]) - in - (* Actually initialize and insert the abstractions *) - let call_id = fresh_fun_call_id () in - let region_can_end _ = true in - let ctx = - create_push_abstractions_from_abs_region_groups - (fun rg_id -> FunCall (call_id, rg_id)) - inst_sg.regions_hierarchy region_can_end compute_abs_avalues ctx - in - - (* Apply the continuation *) - let expr = cf ctx in + let args_with_rtypes = List.combine args inst_sg.inputs in - (* Synthesize the symbolic AST *) - S.synthesize_regular_function_call fid call_id ctx sg regions_hierarchy - abs_ids generics trait_method_generics args args_places ret_spc dest_place - expr + (* Check the type of the input arguments *) + cassert __FILE__ __LINE__ + (List.for_all + (fun ((arg, rty) : typed_value * rty) -> + arg.ty = Subst.erase_regions rty) + args_with_rtypes) + span "The input arguments don't have the proper type"; + (* Check that the input arguments don't contain symbolic values that can't + * be fed to functions (i.e., symbolic values output from function return + * values and which contain borrows of borrows can't be used as function + * inputs *) + sanity_check __FILE__ __LINE__ + (List.for_all + (fun arg -> + not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) + args) + span; + + (* Initialize the abstractions and push them in the context. + * First, we define the function which, given an initialized, empty + * abstraction, computes the avalues which should be inserted inside. + *) + let compute_abs_avalues (abs : abs) (ctx : eval_ctx) : + eval_ctx * typed_avalue list = + (* Project over the input values *) + let ctx, args_projs = + List.fold_left_map + (fun ctx (arg, arg_rty) -> + apply_proj_borrows_on_input_value config span ctx abs.regions + abs.ancestors_regions arg arg_rty) + ctx args_with_rtypes + in + (* Group the input and output values *) + (ctx, List.append args_projs [ ret_av abs.regions ]) + in + (* Actually initialize and insert the abstractions *) + let call_id = fresh_fun_call_id () in + let region_can_end _ = true in + let ctx = + create_push_abstractions_from_abs_region_groups + (fun rg_id -> FunCall (call_id, rg_id)) + inst_sg.regions_hierarchy region_can_end compute_abs_avalues ctx + in + (* Synthesize the symbolic AST *) + let cc = + cc_comp cc + (S.synthesize_regular_function_call fid call_id ctx sg regions_hierarchy + abs_ids generics trait_method_generics args args_places ret_spc + dest_place) in - let cc = comp cc cf_call in (* Move the return value to its destination *) - let cc = comp cc (assign_to_place config meta ret_value dest) in + let ctx, cc = comp cc (assign_to_place config span ret_value dest ctx) in (* End the abstractions which don't contain loans and don't have parent * abstractions. @@ -1499,8 +1499,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config) * retry (because then we might end their children abstractions) *) let abs_ids = ref abs_ids in - let rec end_abs_with_no_loans cf : m_fun = - fun ctx -> + let rec end_abs_with_no_loans ctx = (* Find the abstractions which don't contain loans *) let no_loans_abs, with_loans_abs = List.partition @@ -1512,7 +1511,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config) (* Check if it contains non-ignored loans *) && Option.is_none (InterpreterBorrowsCore - .get_first_non_ignored_aloan_in_abstraction meta abs)) + .get_first_non_ignored_aloan_in_abstraction span abs)) !abs_ids in (* Check if there are abstractions to end *) @@ -1521,35 +1520,36 @@ and eval_function_call_symbolic_from_inst_sig (config : config) abs_ids := with_loans_abs; (* End the abstractions which can be ended *) let no_loans_abs = AbstractionId.Set.of_list no_loans_abs in - let cc = InterpreterBorrows.end_abstractions config meta no_loans_abs in + let ctx, cc = + InterpreterBorrows.end_abstractions config span no_loans_abs ctx + in (* Recursive call *) - let cc = comp cc end_abs_with_no_loans in - (* Continue *) - cc cf ctx) + comp cc (end_abs_with_no_loans ctx)) else (* No abstractions to end: continue *) - cf ctx + (ctx, fun e -> e) in (* Try to end the abstractions with no loans if: * - the option is enabled * - the function returns unit * (see the documentation of {!config} for more information) *) - let cc = - if Config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output - then comp cc end_abs_with_no_loans - else cc + let ctx, cc = + comp cc + (if Config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output + then end_abs_with_no_loans ctx + else (ctx, fun e -> e)) in (* Continue - note that we do as if the function call has been successful, * by giving {!Unit} to the continuation, because we place us in the case * where we haven't panicked. Of course, the translation needs to take the * panic case into account... *) - cc (cf Unit) ctx + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ span cc) (** Evaluate a non-local function call in symbolic mode *) -and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) - (fid : assumed_fun_id) (call : call) (func : fn_ptr) : st_cm_fun = - fun cf ctx -> +and eval_assumed_function_call_symbolic (config : config) (span : Meta.span) + (fid : assumed_fun_id) (call : call) (func : fn_ptr) : stl_cm_fun = + fun ctx -> let generics = func.generics in let args = call.args in let dest = call.dest in @@ -1559,7 +1559,7 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) (List.for_all (fun ty -> not (ty_has_borrows ctx.type_ctx.type_infos ty)) generics.types) - meta; + span; (* There are two cases (and this is extremely annoying): - the function is not box_free @@ -1570,7 +1570,8 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) | 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 meta generics args dest (cf Unit) ctx + let ctx, cc = eval_box_free config span generics args dest ctx in + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ span cc) | _ -> (* "Normal" case: not box_free *) (* In symbolic mode, the behaviour of a function call is completely defined @@ -1580,7 +1581,7 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) match fid with | BoxFree -> (* Should have been treated above *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" | _ -> let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FAssumed fid) @@ -1590,33 +1591,42 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) let tr_self = UnknownTrait __FUNCTION__ in let sg = Assumed.get_assumed_fun_sig fid in let inst_sg = - instantiate_fun_sig meta ctx generics tr_self sg regions_hierarchy + instantiate_fun_sig span ctx generics tr_self sg regions_hierarchy in (sg, regions_hierarchy, inst_sg) in (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config meta + eval_function_call_symbolic_from_inst_sig config span (FunId (FAssumed fid)) sg regions_hierarchy inst_sig generics None args - dest cf ctx + dest ctx (** Evaluate a statement seen as a function body *) -and eval_function_body (config : config) (body : statement) : st_cm_fun = - fun cf ctx -> +and eval_function_body (config : config) (body : statement) : stl_cm_fun = + fun ctx -> log#ldebug (lazy "eval_function_body:"); - let cc = eval_statement config body in - let cf_finish cf res = - log#ldebug (lazy "eval_function_body: cf_finish"); - (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we - * delegate the check to the caller. *) - (* Expand the symbolic values if necessary - we need to do that before - * checking the invariants *) - let cc = greedy_expand_symbolic_values config body.meta in - (* Sanity check *) - let cc = comp_check_ctx cc (Invariants.check_invariants body.meta) in - (* Check if right meta *) - (* Continue *) - cc (cf res) + let ctx_resl, cf_body = eval_statement config body ctx in + let ctx_res_cfl = + List.map + (fun (ctx, res) -> + log#ldebug (lazy "eval_function_body: cf_finish"); + (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we + * delegate the check to the caller. *) + (* Expand the symbolic values if necessary - we need to do that before + * checking the invariants *) + let ctx, cf = greedy_expand_symbolic_values config body.span ctx in + (* Sanity check *) + Invariants.check_invariants body.span ctx; + (* Continue *) + ((ctx, res), cf)) + ctx_resl + in + let ctx_resl, cfl = List.split ctx_res_cfl in + let cf_end el = + match el with + | None -> None + | Some el -> + Some (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el)) in (* Compose and continue *) - comp cc cf_finish cf ctx + (ctx_resl, cc_comp cf_body cf_end) |