package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/src/linksem_zarith/byte_sequence_wrapper.ml.html
Source file byte_sequence_wrapper.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 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
open Buffer open Error open List type byte_sequence = { bytes: Bytes.t; start: int; len: int } let of_bytes b = { bytes = b; start = 0; len = Bytes.length b } let length bs = bs.len let capacity bs = (Bytes.length bs.bytes) - bs.start let empty = { bytes = Bytes.empty; start = 0; len = 0 } let acquire (filename : string) = let ic = open_in_bin filename in let len = in_channel_length ic in let b = Bytes.create len in really_input ic b 0 len; close_in ic; Success (of_bytes b) let serialise (filename : string) bs = let oc = open_out_bin filename in output oc bs.bytes bs.start bs.len; close_out oc; Success () let get bs i = Bytes.get bs.bytes (bs.start + i) let unsafe_get bs i = Bytes.unsafe_get bs.bytes (bs.start + i) let read_char bs = if length bs = 0 then Fail "read_char: sequence is empty" else Success (unsafe_get bs 0, { bs with start = bs.start + 1; len = bs.len - 1 }) let find_byte bs b = match Bytes.index_from_opt bs.bytes bs.start b with | Some i -> let i = i - bs.start in if i < bs.len then Some i else None | None -> None let make len c = of_bytes (Bytes.make len c) let concat l = match l with | [] -> empty | [bs] -> bs | bs::_ -> let buf = Buffer.create bs.len in List.iter (fun bs -> Buffer.add_subbytes buf bs.bytes bs.start bs.len ) l; of_bytes (Buffer.to_bytes buf) let zero_pad_to_length len bs = let pad = bs.len - len in if pad <= 0 then bs else let grow = (capacity bs) - len in let prev_len = Bytes.length bs.bytes in let b = if grow > 0 then Bytes.extend bs.bytes 0 grow else bs.bytes in Bytes.fill b prev_len pad '0'; { bs with bytes = b; len = bs.len + pad } let to_string bs = Bytes.sub_string bs.bytes bs.start bs.len let rec list_init_tailrec_aux acc i n f = if i >= n then acc else list_init_tailrec_aux (f i :: acc) (i+1) n f let list_init len f = List.rev (list_init_tailrec_aux [] 0 len f) (* Note: byte lists are lame *) let to_char_list bs = (* TODO: OCaml >= 4.06 has List.init, use that instead *) list_init bs.len (fun i -> unsafe_get bs i) let from_char_list l = let n = List.length l in let res = Bytes.create n in let rec from_at i = function | [] -> () | c :: xc -> Bytes.unsafe_set res i c; from_at (i+1) xc in from_at 0 l; of_bytes res exception Different of int let compare bs1 bs2 = let d = bs2.len - bs1.len in if d <> 0 then d else if bs1.len = 0 then 0 else try for i = 0 to bs1.len - 1 do let c1 = get bs1 i in let c2 = get bs2 i in let d = (int_of_char c2) - (int_of_char c1) in if d <> 0 then raise (Different d) done; 0 with Different d -> d let equal bs1 bs2 = compare bs1 bs2 = 0 let dropbytes len bs = if len > bs.len then Fail "dropbytes: cannot drop more bytes than are contained in sequence" else (* TODO: maybe shrink the bytes? *) Success { bs with start = bs.start + len; len = bs.len - len } let takebytes len bs = if len > bs.len then Fail "takebytes: cannot take more bytes than are contained in sequence" else Success { bs with len } (* Lem bindings, OCaml implementation *) let big_num_length bs = Nat_big_num.of_int (length bs) let big_num_find_byte bs b= match find_byte bs b with | Some i -> Some (Nat_big_num.of_int i) | None -> None let big_num_make len c = make (Nat_big_num.to_int len) c let big_num_zero_pad_to_length len bs = zero_pad_to_length (Nat_big_num.to_int len) bs let big_num_dropbytes len bs = dropbytes (Nat_big_num.to_int len) bs let big_num_takebytes len bs = takebytes (Nat_big_num.to_int len) bs let takebytes_with_length count bs_length bs = if length bs <> (Nat_big_num.to_int bs_length) then fail "takebytes_with_length: invalid length" else big_num_takebytes count bs (* Lem bindings, generic implementation *) let char_list_of_byte_list l = l let acquire_byte_list filename = match acquire filename with | Success bs -> Success (to_char_list bs) | Fail msg -> Fail msg let serialise_byte_list filename l = serialise filename (from_char_list l)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>