Separate out code used by a pager in OP-TEE