package linksem

  1. Overview
  2. Docs

Source file abi_cheri_mips64_capability.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
(*Generated by Lem from abis/cheri_mips64/abi_cheri_mips64_capability.lem.*)
open Lem_maybe
open Lem_num

open Byte_pattern
open Endianness
open Memory_image
open Missing_pervasives

(*val natural_to_byte_pattern_padded_to : endianness -> natural -> natural -> byte_pattern*)
let natural_to_byte_pattern_padded_to endian width value:(byte_pattern_element)list=
   (let bl = (Memory_image.natural_to_byte_list_padded_to endian width value) in
  Byte_pattern.byte_list_to_byte_pattern bl)

(** Format a CHERI256 capability. *)
(*val abi_cheri_mips64_write_capability_byte_pattern : endianness
  -> maybe natural -> maybe bool -> maybe natural -> maybe natural
  -> maybe natural -> maybe natural -> maybe natural
  -> byte_pattern*)
let abi_cheri_mips64_write_capability_byte_pattern endian
    otype sealed perms uperms cursor base len:(byte_pattern_element)list=
   (let bp = (Byte_pattern.init_byte_pattern( (Nat_big_num.of_int 32))) in

  (* TODO: write other fields too *)

  let bp = ((match cursor with
    | Some cursor ->
      let cursor_bp = (natural_to_byte_pattern_padded_to endian( (Nat_big_num.of_int 8)) cursor) in
      write_byte_pattern bp( (Nat_big_num.of_int 8)) cursor_bp
    | None -> bp
  )) in

  let bp = ((match base with
    | Some base ->
      let base_bp = (natural_to_byte_pattern_padded_to endian( (Nat_big_num.of_int 8)) base) in
      write_byte_pattern bp( (Nat_big_num.of_int 16)) base_bp
    | None -> bp
  )) in

  let bp = ((match len with
    | Some len ->
      let len = (Nat_big_num.sub_nat (natural_of_hex "0xffffffffffffffff") len) in (* TODO: what, why? *)
      let len_bp = (natural_to_byte_pattern_padded_to endian( (Nat_big_num.of_int 8)) len) in
      write_byte_pattern bp( (Nat_big_num.of_int 24)) len_bp
    | None -> bp
  )) in

  bp)