package linksem

You can search for identifiers within the package.

in-package search v0.2.0

A formalisation of the core ELF and DWARF file formats written in Lem

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

Maintainers

L

Linksem Devs <cl-linksem-dev@lists.cam.ac.uk>

Sources

0.8.tar.gz

md5=2075c56715539b3b8f54ae65cc808b8c

sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2

doc/src/linksem_zarith/uint32_wrapper.ml.html

Source file `uint32_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
type uint32 = Nat_big_num.num

(* 2^32 - 1 *)
let max_int =
  Nat_big_num.sub
    (Nat_big_num.pow_int_positive 2 32)
    (Nat_big_num.of_int 1)
;;

let add l r =
  Nat_big_num.modulus (Nat_big_num.add l r) max_int
;;

let of_char (c : char) : uint32 =
  Nat_big_num.of_int (Char.code c)
;;

let of_int (i : int) : uint32 =
  Nat_big_num.modulus (Nat_big_num.of_int i) max_int
;;

let of_bigint (i : Nat_big_num.num) : uint32 =
  Nat_big_num.modulus i max_int
;;

let of_int32 (i : Int32.t) : uint32 =
  Nat_big_num.modulus (Nat_big_num.of_int32 i) max_int
;;

let to_bigint (u : uint32) : Nat_big_num.num = u
;;

let shift_left i s : uint32 =
  Nat_big_num.modulus (Nat_big_num.shift_left i s) max_int
;;

let shift_right i s : uint32 =
  Nat_big_num.modulus (Nat_big_num.shift_right i s) max_int
;;

let logand l r : uint32 =
  Nat_big_num.modulus (Nat_big_num.bitwise_and l r) max_int
;;

let logor l r : uint32 =
  Nat_big_num.modulus (Nat_big_num.bitwise_or l r) max_int
;;

let to_string l : string =
  Nat_big_num.to_string l
;;

let to_char u : char =
  Char.chr (Nat_big_num.to_int u)
;;

let to_int u =
  Nat_big_num.to_int u
;;

let equal l r : bool =
  Nat_big_num.equal l r
;;

let of_string s =
  Nat_big_num.modulus (Nat_big_num.of_string s) max_int
;;

let of_quad (c1: char) (c2: char) (c3: char) (c4: char) : uint32 =
  let b1 = Nat_big_num.of_int (Char.code c1) in
  let b2 = Nat_big_num.shift_left (Nat_big_num.of_int (Char.code c2)) 8 in
  let b3 = Nat_big_num.shift_left (Nat_big_num.of_int (Char.code c3)) 16 in
  let b4 = Nat_big_num.shift_left (Nat_big_num.of_int (Char.code c4)) 24 in
    Nat_big_num.add b1 (Nat_big_num.add b2 (Nat_big_num.add b3 b4))
;;

let of_dual c1 c2 = of_quad c1 c2 '\000' '\000'
;;

let to_bytes u : char * char * char * char =
  let b0 = Char.chr (Nat_big_num.to_int (logand u (Nat_big_num.of_string "255"))) in
  let b1 = Char.chr (Nat_big_num.to_int (shift_right (logand u (Nat_big_num.of_string "65280")) 8)) in
  let b2 = Char.chr (Nat_big_num.to_int (shift_right (logand u (Nat_big_num.of_string "16711680")) 16)) in
  let b3 = Char.chr (Nat_big_num.to_int (shift_right (logand u (Nat_big_num.of_string "4278190080")) 24)) in
    b0, b1, b2, b3
;;

let to_dual_bytes u : char * char =
  let (b3, b2, b1, b0) = to_bytes u in
    b3, b2
;;

package linksem

Install

Dune Dependency

Authors

Maintainers

Sources

doc/src/linksem_zarith/uint32_wrapper.ml.html

Source file uint32_wrapper.ml

Source file `uint32_wrapper.ml`