/*
 * Copyright 2019, Data61
 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
 * ABN 41 687 119 230.
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 */

#pragma once

#include <simple/simple.h>
#include <vka/vka.h>
#include <vspace/vspace.h>

#include <sel4vm/guest_vm.h>

/* ID of the boot vcpu in a VM */
#define BOOT_VCPU 0

/* Initialise/Create VM */
int vm_init(vm_t *vm, vka_t *vka, simple_t *host_simple, vspace_t host_vspace,
            ps_io_ops_t *io_ops, seL4_CPtr host_endpoint, const char *name);

/* Create a VCPU for a given VM */
vm_vcpu_t *vm_create_vcpu(vm_t *vm, int priority);

/* Assign a vcpu with logical target cpu to run on
 * @param[in] vcpu          A handle to the VCPU
 * @param[in] target        Logical target CPU ID
 * @return                  -1 for error, otherwise 0 for success
 */
int vm_assign_vcpu_target(vm_vcpu_t *vcpu, int target_cpu);