camkes/templates/component.environment.start.cakeml

(*
 * Copyright 2018, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(* /*? macros.generated_file_notice() ?*/ *)

open preamble basis

val _ = new_theory "camkesStart";

val _ = translation_extends "basisProg";

val _ = ml_prog_update (open_module "Utils")

val get_word_size_def = process_topdecs `
    fun get_word_size u = /*? macros.get_word_size(options.architecture) ?*/
`;

val int_to_bytes_def = process_topdecs `
    fun int_to_bytes w len = let
        val array = Word8Array.array len (Word8.fromInt 0);
        fun loop i divisor =
            if i = len then
                ()
            else
                let val _ = Word8Array.update array i (Word8.fromInt (w div divisor));
                in loop (i + 1) (divisor * 256)
                end
        val _ = loop 0 1;
        in array end;
`;

(* Read the first `len` bytes of `buf` beginning at `off` into a int *)
val bytes_to_int_def = process_topdecs `
    fun bytes_to_int buf off len = let
        fun loop i acc =
            if i = len then
                acc
            else
                loop (i + 1) (acc * 256 + (Word8.toInt (Word8Array.sub buf (off + len - i - 1))))
        in loop 0 0 end;
`;

(* Read the a nul-terminated string from `buf` beginning at `off` *)
val read_c_string_def = process_topdecs `
  fun read_c_string buf off len = let
    fun nul_byte_idx i =
      if i = len orelse Word8Array.sub buf i = Word8.fromInt 0 then
        i
      else
        nul_byte_idx (i + 1);
    val str_len = nul_byte_idx off - off;
    in (Word8Array.substring buf off str_len, str_len) end;
`;

(* Convert a string to a Word8Array *)
val string_to_bytes_def = process_topdecs `
  fun string_to_bytes str = let
    val len = String.size str;
    val result = Word8Array.array len (Word8.fromInt 0);
    val _ = Word8Array.copyVec str 0 len result 0;
    in result end;
`;

val seL4_ReplyRecv_def = process_topdecs `
    fun seL4_ReplyRecv ep send_length ipcbuf = let
        val word_size = /*? macros.get_word_size(options.architecture) ?*/;
        val _ = Word8Array.copy (int_to_bytes ep word_size) 0 word_size ipcbuf 1;
        val _ = Word8Array.copy (int_to_bytes send_length word_size) 0 word_size ipcbuf (1 + word_size);
        val _ = #(seL4_ReplyRecv) "" ipcbuf;
        val len = bytes_to_int ipcbuf 1 word_size;
        val badge = bytes_to_int ipcbuf (1 + word_size) word_size;
        in (len, badge) end;
`;

val seL4_Recv_def = process_topdecs `
    fun seL4_Recv ep ipcbuf = let
        val word_size = /*? macros.get_word_size(options.architecture) ?*/;
        val _ = Word8Array.copy (int_to_bytes ep word_size) 0 word_size ipcbuf 1;
        val _ = #(seL4_Recv) "" ipcbuf;
        val len = bytes_to_int ipcbuf 1 word_size;
        val badge = bytes_to_int ipcbuf (1 + word_size) word_size;
        in (len, badge) end;
`;

val seL4_Send_def = process_topdecs `
    fun seL4_Send ep send_length ipcbuf = let
        val word_size = /*? macros.get_word_size(options.architecture) ?*/;
        val _ = Word8Array.copy (int_to_bytes ep word_size) 0 word_size ipcbuf 1;
        val _ = Word8Array.copy (int_to_bytes send_length 8) 0 word_size ipcbuf (1 + word_size);
        val _ = #(seL4_Send) "" ipcbuf;
        in () end;
`;

val seL4_Wait_def = process_topdecs `
    fun seL4_Wait src = let
        val word_size = /*? macros.get_word_size(options.architecture) ?*/;
        val buf = Word8Array.array (1 + word_size)  (Word8.fromInt 0);
        val _ = Word8Array.copy (int_to_bytes src word_size) 0 word_size buf 1;
        val _ = #(seL4_Wait) "" buf;
        val badge = bytes_to_int buf 1 word_size;
        in badge end;
`;

val camkes_declare_reply_cap_def = process_topdecs `
    fun camkes_declare_reply_cap slot = let
        val word_size = /*? macros.get_word_size(options.architecture) ?*/;
        val buf = Word8Array.array (1 + word_size) (Word8.fromInt 0);
        val _ = Word8Array.copy (int_to_bytes slot word_size) 0 word_size buf 1;
        val _ = #(camkes_declare_reply_cap) "" buf;
        in () end;
`;

val clear_tls_reply_cap_in_tcb_def = process_topdecs `
    fun clear_tls_reply_cap_in_tcb u = let
        val buf = Word8Array.array 2 (Word8.fromInt 0);
        val _ = #(clear_tls_reply_cap_in_tcb) "" buf;
        in (Word8Array.sub buf 1) <> (Word8.fromInt 0) end;
`;

val fail_def = process_topdecs `
    fun fail msg = let
        val _ = TextIO.print (msg ^ "\n");
        val _ = #(fail) "" (Word8Array.array 0 (Word8.fromInt 0));
        in () end;
`;

val _ = app append_prog [
    int_to_bytes_def,
    bytes_to_int_def,
    read_c_string_def,
    string_to_bytes_def,
    get_word_size_def,
    fail_def,
    seL4_Recv_def,
    seL4_ReplyRecv_def,
    seL4_Send_def,
    seL4_Wait_def,
    camkes_declare_reply_cap_def,
    clear_tls_reply_cap_in_tcb_def
];

val _ = ml_prog_update (close_module NONE);

val _ = export_theory ();