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_pattern.ml.html
Source file byte_pattern.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 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
(*Generated by Lem from byte_pattern.lem.*) open Lem_assert_extra open Lem_basic_classes open Lem_bool open Lem_list open Lem_maybe open Lem_num open Lem_string open Byte_sequence open Missing_pervasives open Show (** A byte pattern element can be undefined if it doesn't have a known fixed value. *) type byte_pattern_element = char option (* TODO: replace with two byte sequences (one used as a mask) *) type byte_pattern = byte_pattern_element list (*val string_of_byte_pattern : byte_pattern -> string*) let rec string_of_byte_pattern bp:string= (let parts = (Lem_list.map (fun maybe_b -> (match maybe_b with | None -> "--" | Some b -> hex_string_of_byte b ) ) bp) in let (_, s) = (List.fold_left (fun (n, s) part -> let s = (if Nat_big_num.equal (Nat_big_num.modulus n( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 0)) && not (s = "") then s ^ (" " ^ part) else s ^ part) in ( Nat_big_num.add n( (Nat_big_num.of_int 1)), s) ) (( (Nat_big_num.of_int 0) : Nat_big_num.num), "") parts) in s) (*val make_byte_pattern_revacc : byte_pattern -> list byte -> list bool -> byte_pattern*) let rec make_byte_pattern_revacc revacc bytes cares:((char)option)list= ((match bytes with [] -> List.rev revacc | b :: bs -> (match cares with care :: more -> make_byte_pattern_revacc ((if not care then None else Some b) :: revacc) bs more | _ -> failwith "make_byte_pattern: unequal length" ) )) (*val make_byte_pattern : list byte -> list bool -> byte_pattern*) let rec make_byte_pattern bytes cares:(byte_pattern_element)list= (make_byte_pattern_revacc [] bytes cares) (*val byte_list_to_byte_pattern : list byte -> byte_pattern*) let byte_list_to_byte_pattern bl:((char)option)list= (Lem_list.map (fun b -> Some b) bl) (*val init_byte_pattern : natural -> byte_pattern*) let init_byte_pattern len:((char)option)list= (Lem_list.replicate (Nat_big_num.to_int len) None) (*val byte_pattern_length : byte_pattern -> natural*) let byte_pattern_length bp:Nat_big_num.num= (Nat_big_num.of_int (List.length bp)) (*val relax_byte_pattern_revacc : byte_pattern -> byte_pattern -> list bool -> byte_pattern*) let rec relax_byte_pattern_revacc revacc bytes cares:((char)option)list= ((match bytes with [] -> List.rev revacc | b :: bs -> (match cares with care :: more -> relax_byte_pattern_revacc ((if not care then None else b) :: revacc) bs more | _ -> failwith ("relax_byte_pattern: unequal length") ) )) (*val relax_byte_pattern : byte_pattern -> list bool -> byte_pattern*) let rec relax_byte_pattern bytes cares:(byte_pattern_element)list= (relax_byte_pattern_revacc [] bytes cares) type pad_fn = Nat_big_num.num -> char list (*val concretise_byte_pattern' : list byte -> natural -> byte_pattern -> pad_fn -> list byte*) let rec concretise_byte_pattern' rev_acc acc_pad bs pad:(char)list= ((match bs with [] -> let padding_bytes = (if Nat_big_num.greater acc_pad( (Nat_big_num.of_int 0)) then pad acc_pad else []) in List.rev ( List.rev_append (List.rev (List.rev padding_bytes)) rev_acc) | Some(b) :: more -> (* flush accumulated padding *) let padding_bytes = (if Nat_big_num.greater acc_pad( (Nat_big_num.of_int 0)) then pad acc_pad else []) in concretise_byte_pattern' (b :: ( List.rev_append (List.rev (List.rev padding_bytes)) rev_acc))( (Nat_big_num.of_int 0)) more pad | None :: more -> concretise_byte_pattern' rev_acc (Nat_big_num.add acc_pad( (Nat_big_num.of_int 1))) more pad )) (*val concretise_byte_pattern : byte_pattern -> pad_fn -> byte_sequence*) let rec concretise_byte_pattern pb pad:Byte_sequence_wrapper.byte_sequence= ( (* TODO: don't use lists of bytes *)byte_sequence_of_byte_list (concretise_byte_pattern' []( (Nat_big_num.of_int 0)) pb pad)) (*val byte_option_matches_byte : maybe byte -> byte -> bool*) let byte_option_matches_byte optb b:bool= ((match optb with None -> true | Some some -> some = b )) (*val byte_list_matches_pattern : byte_pattern -> list byte -> bool*) let rec byte_list_matches_pattern pattern bytes:bool= ((match pattern with [] -> true | optbyte :: more -> (match bytes with [] -> false | abyte :: morebytes -> byte_option_matches_byte optbyte abyte && byte_list_matches_pattern more morebytes ) )) (*val append_to_byte_pattern_at_offset : natural -> byte_pattern -> byte_pattern -> byte_pattern*) let append_to_byte_pattern_at_offset offset pat1 pat2:((char)option)list= (let pad_length = (Nat_big_num.sub_nat offset (Missing_pervasives.length pat1)) in if Nat_big_num.less pad_length( (Nat_big_num.of_int 0)) then failwith "can't append at offset already used" else List.rev_append (List.rev (List.rev_append (List.rev pat1) (Lem_list.replicate (Nat_big_num.to_int pad_length) None))) pat2) (*val accum_pattern_possible_starts_in_one_byte_sequence : byte_pattern -> nat -> list byte -> nat -> natural -> list natural -> list natural*) let rec accum_pattern_possible_starts_in_one_byte_sequence pattern pattern_len seq seq_len offset accum:(Nat_big_num.num)list= ( (* let _ = Missing_pervasives.errs ("At offset " ^ (show offset) ^ "... ") in *)(match pattern with [] -> (* let _ = Missing_pervasives.errs ("terminating with hit (empty pattern)\n") in *) offset :: accum | bpe :: more_bpes -> (* nonempty, so check for nonempty seq *) (match seq with [] -> (*let _ = Missing_pervasives.errs ("terminating with miss (empty pattern)\n") in *) accum (* ran out of bytes in the sequence, so no match *) | byte1 :: more_bytes -> let matched_this_byte = (byte_option_matches_byte bpe byte1) in (* let _ = Missing_pervasives.errs ("Byte " ^ (show byte) ^ " matched " ^ (show byte_pattern) ^ "? " ^ (show matched_this_byte) ^ "; ") in *) let sequence_long_enough = (seq_len >= pattern_len) in (* let _ = Missing_pervasives.errs ("enough bytes remaining (" ^ (show seq_len) ^ ") to match rest of pattern (" ^ (show pattern_len) ^ ")? " ^ (show sequence_long_enough) ^ "; ") in *) let matched_here = (matched_this_byte && (sequence_long_enough && byte_list_matches_pattern more_bpes more_bytes)) in (* let _ = Missing_pervasives.errs ("matched pattern anchored here? " ^ (show matched_this_byte) ^ "\n") in *) accum_pattern_possible_starts_in_one_byte_sequence pattern pattern_len more_bytes ( Nat_num.nat_monus seq_len 1) ( Nat_big_num.add offset( (Nat_big_num.of_int 1))) (if matched_here then offset :: accum else accum) ) )) (*val byte_pattern_of_byte_sequence : byte_sequence -> byte_pattern*) let byte_pattern_of_byte_sequence seq:((char)option)list= (let l = (byte_list_of_byte_sequence seq) in Lem_list.map (fun b -> Some b) l) (* Prefer using byte sequences when possible *) (*val byte_pattern_to_byte_list : byte_pattern -> list byte*) let byte_pattern_to_byte_list bp:(char)list= (Lem_list.map (fun maybe_b -> (match maybe_b with | Some b -> b | None -> failwith "byte_pattern_to_byte_sequence: attempt to read a masked byte" ) ) bp) (*val byte_pattern_to_byte_sequence : byte_pattern -> byte_sequence*) let byte_pattern_to_byte_sequence bp:Byte_sequence_wrapper.byte_sequence= (let l = (byte_pattern_to_byte_list bp) in byte_sequence_of_byte_list l) (*val byte_pattern_skip : natural -> byte_pattern -> byte_pattern*) let rec byte_pattern_skip offset bp:((char)option)list= (if Nat_big_num.less offset( (Nat_big_num.of_int 0)) then failwith "byte_pattern_skip: cannot skip a negative number of bytes" else if Nat_big_num.equal offset( (Nat_big_num.of_int 0)) then bp else (match bp with | _ :: bp -> byte_pattern_skip ( Nat_big_num.sub_nat offset( (Nat_big_num.of_int 1))) bp | [] -> failwith "byte_pattern_skip: skipped past end" )) (*val write_byte_pattern : byte_pattern -> natural -> byte_pattern -> byte_pattern*) let write_byte_pattern bp offset sub_bp:((char)option)list= (if (listEqualBy (Lem.option_equal (=)) sub_bp []) then bp else let len = (List.length sub_bp) in let (prefix, bp) = (Lem_list.split_at (Nat_big_num.to_int offset) bp) in let (old, suffix) = (Lem_list.split_at len bp) in (* We don't want to change the byte pattern length *) let _ = (if (listEqualBy (Lem.option_equal (=)) suffix []) && not ((List.length old) = len) then failwith "write_byte_pattern: write past end" else ()) in List.rev_append (List.rev (List.rev_append (List.rev prefix) sub_bp)) suffix) (*val read_byte_pattern : byte_pattern -> natural -> natural -> byte_pattern*) let read_byte_pattern bp offset len:((char)option)list= (Lem_list.take (Nat_big_num.to_int len) (Lem_list.drop (Nat_big_num.to_int offset) bp))
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>