summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--cheri/cheri_prelude_128.sail4
-rw-r--r--cheri/cheri_prelude_256.sail4
-rw-r--r--lib/ocaml_rts/sail_lib.ml4
-rw-r--r--lib/prelude.sail68
-rw-r--r--mips_new_tc/mips_prelude.sail4
-rw-r--r--mips_new_tc/mips_wrappers.sail4
-rw-r--r--src/gen_lib/sail_operators.lem49
-rw-r--r--src/gen_lib/sail_operators_mwords.lem3
-rw-r--r--src/gen_lib/sail_values.lem102
-rw-r--r--src/rewriter.ml4
-rw-r--r--src/type_check.ml2
11 files changed, 133 insertions, 115 deletions
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index f1f33a56..5e63221e 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -35,8 +35,8 @@
(* 128 bit cap + tag *)
typedef CapReg = bit[129]
-val cast bool -> bit effect pure cast_bool_bit
-val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec
+val cast extern bool -> bit effect pure cast_bool_bit
+val cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec
val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec
function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v)
val extern bool -> bool effect pure not
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index 7cf3d69c..7b42020d 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -35,8 +35,8 @@
(* 256 bit cap + tag *)
typedef CapReg = bit[257]
-val cast bool -> bit effect pure cast_bool_bit
-val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec
+val cast extern bool -> bit effect pure cast_bool_bit
+val cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec
val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec
function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v)
val extern bool -> bool effect pure not
diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml
index 9b1bbc30..176c1124 100644
--- a/lib/ocaml_rts/sail_lib.ml
+++ b/lib/ocaml_rts/sail_lib.ml
@@ -376,6 +376,10 @@ let read_ram (addr_size, data_size, hex_ram, addr) =
in
read_byte data_size
+let rec reverse_endianness bits =
+ if List.length bits <= 8 then bits else
+ reverse_endianness (drop 8 bits) @ (take 8 bits)
+
(* FIXME: Casts can't be externed *)
let zcast_unit_vec x = [x]
diff --git a/lib/prelude.sail b/lib/prelude.sail
index 36ccaca0..8cc1b86d 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -1,7 +1,7 @@
-val cast forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned
+val cast extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned
-val forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0 - (2**('m - 1)):2**('m - 1) - 1|] effect pure signed
+val extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0 - (2**('m - 1)):2**('m - 1) - 1|] effect pure signed
val forall Num 'n, Num 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec
@@ -44,7 +44,7 @@ val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, Type 'a, 'l1 >=
val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0.
(vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,bit> effect pure bitvector_append = "bitvector_concat"
-val (list<bit>, list<bit>) -> list<bit> effect pure list_append
+val extern (list<bit>, list<bit>) -> list<bit> effect pure list_append
overload append [bitvector_append; vector_append; list_append]
@@ -58,17 +58,17 @@ val extern forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l
overload vector_update [bitvector_update_dec; bitvector_update_inc; vector_update_dec; vector_update_inc]
(* Implicit register dereferencing *)
-val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref
+val cast extern forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref
(* Bitvector duplication *)
-val forall Num 'n. (bit, [:'n:]) -> vector<'n - 1,'n,dec,bit> effect pure duplicate
+val extern forall Num 'n. (bit, [:'n:]) -> vector<'n - 1,'n,dec,bit> effect pure duplicate
-val (bit, int) -> list<bit> effect pure duplicate_to_list
+val extern (bit, int) -> list<bit> effect pure duplicate_to_list
val extern forall Num 'n, Num 'm, Num 'o, Order 'ord.
(vector<'o,'n,'ord,bit>, [:'m:]) -> vector<'o,'m*'n,'ord,bit> effect pure duplicate_bits
-val forall Num 'n, Num 'o, Order 'ord.
+val extern forall Num 'n, Num 'o, Order 'ord.
(vector<'o,'n,'ord,bit>, int) -> list<bit> effect pure duplicate_bits_to_list
overload (deinfix ^^) [duplicate; duplicate_bits; duplicate_to_list; duplicate_bits_to_list]
@@ -98,7 +98,7 @@ val extern forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o.
vector<'n, 'm, 'ord, 'a> -> vector<'p, 'o, 'ord, 'a> effect pure mask
(* Adjust the start index of a decreasing bitvector *)
-val cast forall Num 'n, Num 'm, 'n >= 'm - 1.
+val cast extern forall Num 'n, Num 'm, 'n >= 'm - 1.
vector<'n,'m,dec,bit> -> vector<'m - 1,'m,dec,bit>
effect pure norm_dec
@@ -114,14 +114,26 @@ val cast forall Num 'n, Num 'l. [:0:] -> vector<'n,'l,inc,bit> effect pure cast_
val cast forall Num 'n, Num 'l. [:1:] -> vector<'n,'l,inc,bit> effect pure cast_1_vec_inc
val cast forall Num 'n, Num 'l. [|0:1|] -> vector<'n,'l,inc,bit> effect pure cast_01_vec_inc
-val cast forall Num 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool
-val cast bit -> bool effect pure cast_bit_bool
+val cast extern forall Num 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool
+val cast extern bit -> bool effect pure cast_bit_bool
val cast forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. bit -> vector<'n,'m,dec,bit> effect pure cast_bit_vec
+(* Cast from bitvectors to bit lists *)
+
+val extern forall Num 'n, Num 'l, Order 'ord. vector<'n,'l,'ord,bit> -> list<bit> effect pure cast_vec_bl
+
(* MSB *)
val forall Num 'n, Num 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect pure most_significant
+(* Endianness *)
+val extern forall Num 'n, Num 'm, Order 'ord. vector<'n, 8 * 'm, 'ord, bit> -> vector<'n, 8 * 'm, 'ord, bit> effect pure reverse_endianness
+
+(* List functions *)
+
+val extern forall Type 'a. (int, list<'a>) -> list<'a> effect pure list_take
+val extern forall Type 'a. (int, list<'a>) -> list<'a> effect pure list_drop
+
(* Arithmetic *)
val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
@@ -131,16 +143,16 @@ val extern (nat, nat) -> nat effect pure add_nat = "add_int"
val extern (int, int) -> int effect pure add_int
-val forall Num 'n, Num 'o, Order 'ord.
+val extern forall Num 'n, Num 'o, Order 'ord.
(vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec
-val forall Num 'n, Num 'o, Order 'ord.
+val extern forall Num 'n, Num 'o, Order 'ord.
(vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure add_vec_int
-val forall Num 'n, Num 'o, Order 'ord.
+val extern forall Num 'n, Num 'o, Order 'ord.
(int, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_int_vec
-val forall Num 'n, Num 'o, Order 'ord.
+val extern forall Num 'n, Num 'o, Order 'ord.
(vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec
val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
@@ -148,13 +160,13 @@ val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
val extern (int, int) -> int effect pure sub_int = "sub_int"
-val forall Num 'n, Num 'm, Order 'ord.
+val extern forall Num 'n, Num 'm, Order 'ord.
(vector<'n,'m,'ord,bit>, int) -> vector<'n,'m,'ord,bit> effect pure sub_vec_int
-val forall Num 'n, Num 'o, Order 'ord.
+val extern forall Num 'n, Num 'o, Order 'ord.
(vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure sub_vec
-val forall Num 'n, Num 'o, Order 'ord.
+val extern forall Num 'n, Num 'o, Order 'ord.
(vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure sub_underflow_vec
overload (deinfix +) [
@@ -195,24 +207,24 @@ overload (deinfix *_s) [
mult_svec
]
-val extern (bool, bool) -> bool effect pure bool_xor
+val extern (bool, bool) -> bool effect pure xor_bool
val extern forall Num 'n, Num 'o, Order 'ord.
(vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure xor_vec = "bitwise_xor"
overload (deinfix ^) [
- bool_xor;
+ xor_bool;
xor_vec
]
-val forall Num 'n, Num 'o, Order 'ord.
+val extern forall Num 'n, Num 'o, Order 'ord.
(vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure shiftl
overload (deinfix <<) [
shiftl
]
-val forall Num 'n, Num 'o, Order 'ord.
+val extern forall Num 'n, Num 'o, Order 'ord.
(vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure shiftr
overload (deinfix >>) [
@@ -220,9 +232,9 @@ overload (deinfix >>) [
]
(* Boolean operators *)
-val extern bool -> bool effect pure bool_not = "not"
-val extern (bool, bool) -> bool effect pure bool_or
-val extern (bool, bool) -> bool effect pure bool_and
+val extern bool -> bool effect pure not_bool = "not"
+val extern (bool, bool) -> bool effect pure or_bool
+val extern (bool, bool) -> bool effect pure and_bool
val extern forall Num 'n, Num 'm, Order 'ord.
vector<'n,'m,'ord,bit> -> vector<'n,'m,'ord,bit> effect pure bitwise_not
@@ -233,9 +245,9 @@ val extern forall Num 'n, Num 'm, Order 'ord.
val extern forall Num 'n, Num 'm, Order 'ord.
(vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> vector<'n,'m,'ord,bit> effect pure bitwise_or
-overload ~ [bool_not; bitwise_not]
-overload (deinfix &) [bool_and; bitwise_and]
-overload (deinfix |) [bool_or; bitwise_or]
+overload ~ [not_bool; bitwise_not]
+overload (deinfix &) [and_bool; bitwise_and]
+overload (deinfix |) [or_bool; bitwise_or]
(* Equality *)
@@ -314,7 +326,7 @@ val extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [:'m:] e
overload length [bitvector_length; vector_length; list_length]
-val cast forall Num 'n. [:'n:] -> [|'n|] effect pure upper
+val cast extern forall Num 'n. [:'n:] -> [|'n|] effect pure upper
typedef option = const union forall Type 'a. {
None;
diff --git a/mips_new_tc/mips_prelude.sail b/mips_new_tc/mips_prelude.sail
index 128c63d8..c026c85f 100644
--- a/mips_new_tc/mips_prelude.sail
+++ b/mips_new_tc/mips_prelude.sail
@@ -577,7 +577,7 @@ function (bool) isAddressAligned ((bit[64]) addr, (WordType) wordType) =
let a = unsigned(addr) in
((a quot alignment_width) == (a + wordWidthBytes(wordType) - 1) quot alignment_width)
-val forall Nat 'W, 'W >= 1. ([:'W:], bit[8 * 'W]) -> bit[8 * 'W] effect pure reverse_endianness'
+(*val forall Nat 'W, 'W >= 1. ([:'W:], bit[8 * 'W]) -> bit[8 * 'W] effect pure reverse_endianness'
function rec forall Nat 'W, 'W >= 1. bit[8 * 'W] reverse_endianness' (w, value) =
{
@@ -592,7 +592,7 @@ val forall Nat 'W, 'W >= 1. bit[8 * 'W] -> bit[8 * 'W] effect pure reverse_endia
function rec forall Nat 'W, 'W >= 1. bit[8 * 'W] reverse_endianness ((bit[8 * 'W]) value) =
{
reverse_endianness'(sizeof 'W, value)
-}
+}*)
function forall Nat 'n, 1 <= 'n, 'n <= 8. (bit[8 * 'n]) effect { rmem } MEMr_wrapper ((bit[64]) addr, ([:'n:]) size) =
if (addr == 0x000000007f000000) then
diff --git a/mips_new_tc/mips_wrappers.sail b/mips_new_tc/mips_wrappers.sail
index c5eb6cf4..70033977 100644
--- a/mips_new_tc/mips_wrappers.sail
+++ b/mips_new_tc/mips_wrappers.sail
@@ -38,7 +38,7 @@
val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> unit effect {eamem, wmv, wreg} MEMw_wrapper
function unit MEMw_wrapper((bit[64]) addr, ([:'n:]) size, (bit[8 * 'n]) data) =
- let ledata = reverse_endianness'(sizeof 'n, data) in
+ let ledata = reverse_endianness(data) in
if (addr == 0x000000007f000000) then
{
UART_WDATA := ledata[7..0];
@@ -53,7 +53,7 @@ val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> bool effe
function bool MEMw_conditional_wrapper(addr, size, data) =
{
MEMea_conditional(addr, size);
- MEMval_conditional(addr, size, reverse_endianness'(sizeof 'n, data))
+ MEMval_conditional(addr, size, reverse_endianness(data))
}
function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 524d7ef6..826ea98f 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -39,6 +39,7 @@ let cast_vec_bool v = bitU_to_bool (extract_only_element v)
let cast_bit_vec_basic (start, len, b) = Vector (repeat [b] len) start false
let cast_boolvec_bitvec (Vector bs start inc) =
Vector (List.map bool_to_bitU bs) start inc
+let cast_vec_bl (Vector bs start inc) = bs
let pp_bitu_vector (Vector elems start inc) =
let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
@@ -50,8 +51,6 @@ let most_significant = function
| _ -> failwith "most_significant applied to empty vector"
end
-let bitwise_not_bitlist = List.map bitwise_not_bit
-
let bitwise_not (Vector bs start is_inc) =
Vector (bitwise_not_bitlist bs) start is_inc
@@ -63,18 +62,6 @@ let bitwise_and = bitwise_binop (&&)
let bitwise_or = bitwise_binop (||)
let bitwise_xor = bitwise_binop xor
-(*let unsigned (Vector bs _ _) : integer =
- let (sum,_) =
- List.foldr
- (fun b (acc,exp) ->
- match b with
- | B1 -> (acc + integerPow 2 exp,exp + 1)
- | B0 -> (acc, exp + 1)
- | BU -> failwith "unsigned: vector has undefined bits"
- end)
- (0,0) bs in
- sum*)
-
let unsigned_big = unsigned
let signed v : integer =
@@ -136,40 +123,9 @@ let get_min_representable_in _ (n : integer) : integer =
else if n = 5 then min_5
else 0 - (integerPow 2 (natFromInteger n))
-val to_bin_aux : natural -> list bitU
-let rec to_bin_aux x =
- if x = 0 then []
- else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
-let to_bin n = List.reverse (to_bin_aux n)
-
-val pad_zero : list bitU -> integer -> list bitU
-let rec pad_zero bits n =
- if n <= 0 then bits else pad_zero (B0 :: bits) (n -1)
-
-
-let rec add_one_bit_ignore_overflow_aux bits = match bits with
- | [] -> []
- | B0 :: bits -> B1 :: bits
- | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
- | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
-end
-
-let add_one_bit_ignore_overflow bits =
- List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
-
-
let to_norm_vec is_inc ((len : integer),(n : integer)) =
let start = if is_inc then 0 else len - 1 in
- let bits = to_bin (naturalFromInteger (abs n)) in
- let len_bits = integerFromNat (List.length bits) in
- let longer = len - len_bits in
- let bits' =
- if longer < 0 then drop (natFromInteger (abs (longer))) bits
- else pad_zero bits longer in
- if n > (0 : integer)
- then Vector bits' start is_inc
- else Vector (add_one_bit_ignore_overflow (bitwise_not_bitlist bits'))
- start is_inc
+ Vector (bits_of_int (len, n)) start is_inc
let to_vec_big = to_norm_vec
@@ -451,7 +407,6 @@ let gt = compare_op (>)
let lteq = compare_op (<=)
let gteq = compare_op (>=)
-
let compare_op_vec op sign (l,r) =
let (l',r') = (to_num sign l, to_num sign r) in
compare_op op (l',r')
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 8fb55137..74d0acf7 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -65,7 +65,7 @@ let bvslice_raw bs i j =
val bvupdate_aux : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> list bitU -> bitvector 'a
let bvupdate_aux is_inc start bs i j bs' =
let bits = update_aux is_inc start (List.map to_bitU (bitlistFromWord bs)) i j bs' in
- wordFromBitlist (List.map from_bitU bits)
+ wordFromBitlist (List.map of_bitU bits)
(*let iN = natFromInteger i in
let jN = natFromInteger j in
let startN = natFromInteger start in
@@ -110,6 +110,7 @@ let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
let cast_bit_vec_basic (start, len, b) = vec_to_bvec (Vector [b] start false)
let cast_boolvec_bitvec (Vector bs start inc) =
vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc)
+let cast_vec_bl v = List.map bool_to_bitU (bitlistFromWord v)
let pp_bitu_vector (Vector elems start inc) =
let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 45b73ab5..bd18cf81 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -33,11 +33,14 @@ let negate_real r = realNegate r
let abs_real r = realAbs r
let power_real (b, e) = realPowInteger b e
-let bool_or (l, r) = (l || r)
-let bool_and (l, r) = (l && r)
-let bool_xor (l, r) = xor l r
+let or_bool (l, r) = (l || r)
+let and_bool (l, r) = (l && r)
+let xor_bool (l, r) = xor l r
let list_append (l, r) = l ++ r
+let list_length xs = integerFromNat (List.length xs)
+let list_take (n, xs) = List.take (natFromInteger n) xs
+let list_drop (n, xs) = List.drop (natFromInteger n) xs
val repeat : forall 'a. list 'a -> integer -> list 'a
let rec repeat xs n =
@@ -70,12 +73,12 @@ end
class (BitU 'a)
val to_bitU : 'a -> bitU
- val from_bitU : bitU -> 'a
+ val of_bitU : bitU -> 'a
end
instance (BitU bitU)
let to_bitU b = b
- let from_bitU b = b
+ let of_bitU b = b
end
let bitU_to_bool = function
@@ -88,7 +91,7 @@ let bool_to_bitU b = if b then B1 else B0
instance (BitU bool)
let to_bitU = bool_to_bitU
- let from_bitU = bitU_to_bool
+ let of_bitU = bitU_to_bool
end
let cast_bit_bool = bitU_to_bool
@@ -153,6 +156,56 @@ let inline (|.) x y = bitwise_or_bit (x,y)
val (+.) : bitU -> bitU -> bitU
let inline (+.) x y = bitwise_xor_bit (x,y)
+val to_bin_aux : natural -> list bitU
+let rec to_bin_aux x =
+ if x = 0 then []
+ else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
+let to_bin n = List.reverse (to_bin_aux n)
+
+val of_bin : list bitU -> natural
+let of_bin bits =
+ let (sum,_) =
+ List.foldr
+ (fun b (acc,exp) ->
+ match b with
+ | B1 -> (acc + naturalPow 2 exp, exp + 1)
+ | B0 -> (acc, exp + 1)
+ | BU -> failwith "of_bin: bitvector has undefined bits"
+ end)
+ (0,0) bits in
+ sum
+
+val bitlist_to_integer : list bitU -> integer
+let bitlist_to_integer bs = integerFromNatural (of_bin bs)
+
+val pad_zero : list bitU -> integer -> list bitU
+let rec pad_zero bits n =
+ if n <= 0 then bits else pad_zero (B0 :: bits) (n -1)
+
+let bitwise_not_bitlist = List.map bitwise_not_bit
+
+let rec add_one_bit_ignore_overflow_aux bits = match bits with
+ | [] -> []
+ | B0 :: bits -> B1 :: bits
+ | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
+ | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
+end
+
+let add_one_bit_ignore_overflow bits =
+ List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
+
+let bits_of_nat ((len : integer),(n : natural)) =
+ let bits = to_bin n in
+ let len_bits = integerFromNat (List.length bits) in
+ let longer = len - len_bits in
+ if longer < 0 then drop (natFromInteger (abs (longer))) bits
+ else pad_zero bits longer
+
+let bits_of_int ((len : integer),(n : integer)) =
+ let bits = bits_of_nat (len, naturalFromInteger (abs n)) in
+ if n > (0 : integer)
+ then bits
+ else (add_one_bit_ignore_overflow (bitwise_not_bitlist bits))
(*** Vectors *)
@@ -292,47 +345,34 @@ class (Bitvector 'a)
val set_bits : bool -> integer -> 'a -> integer -> integer -> list bitU -> 'a
end
-val bitlist_to_integer : list bitU -> integer
-let bitlist_to_integer bs =
- let (sum,_) =
- List.foldr
- (fun b (acc,exp) ->
- match b with
- | B1 -> (acc + integerPow 2 exp,exp + 1)
- | B0 -> (acc, exp + 1)
- | BU -> failwith "unsigned: vector has undefined bits"
- end)
- (0,0) bs in
- sum
-
instance forall 'a. BitU 'a => (Bitvector (list 'a))
let bits_of v = List.map to_bitU v
- let of_bits v = List.map from_bitU v
+ let of_bits v = List.map of_bitU v
let unsigned v = bitlist_to_integer (List.map to_bitU v)
let get_bit is_inc start v n = to_bitU (access_aux is_inc start v n)
- let set_bit is_inc start v n b = update_aux is_inc start v n n [from_bitU b]
+ let set_bit is_inc start v n b = update_aux is_inc start v n n [of_bitU b]
let get_bits is_inc start v i j = List.map to_bitU (slice_aux is_inc start v i j)
- let set_bits is_inc start v i j v' = update_aux is_inc start v i j (List.map from_bitU v')
+ let set_bits is_inc start v i j v' = update_aux is_inc start v i j (List.map of_bitU v')
end
instance forall 'a. BitU 'a => (Bitvector (vector 'a))
let bits_of v = List.map to_bitU (get_elems v)
- let of_bits v = Vector (List.map from_bitU v) (integerFromNat (List.length v) - 1) false
+ let of_bits v = Vector (List.map of_bitU v) (integerFromNat (List.length v) - 1) false
let unsigned v = unsigned (get_elems v)
let get_bit is_inc start v n = to_bitU (access v n)
- let set_bit is_inc start v n b = update_pos v n (from_bitU b)
+ let set_bit is_inc start v n b = update_pos v n (of_bitU b)
let get_bits is_inc start v i j = List.map to_bitU (get_elems (slice v i j))
- let set_bits is_inc start v i j v' = update v i j (Vector (List.map from_bitU v') (integerFromNat (List.length v') - 1) false)
+ let set_bits is_inc start v i j v' = update v i j (Vector (List.map of_bitU v') (integerFromNat (List.length v') - 1) false)
end
instance forall 'a. Size 'a => (Bitvector (mword 'a))
let bits_of v = List.map to_bitU (bitlistFromWord v)
- let of_bits v = wordFromBitlist (List.map from_bitU v)
+ let of_bits v = wordFromBitlist (List.map of_bitU v)
let unsigned v = unsignedIntegerFromWord v
let get_bit is_inc start v n = to_bitU (access_aux is_inc start (bitlistFromWord v) n)
- let set_bit is_inc start v n b = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) n n [from_bitU b])
+ let set_bit is_inc start v n b = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) n n [of_bitU b])
let get_bits is_inc start v i j = slice_aux is_inc start (List.map to_bitU (bitlistFromWord v)) i j
- let set_bits is_inc start v i j v' = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) i j (List.map from_bitU v'))
+ let set_bits is_inc start v i j v' = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) i j (List.map of_bitU v'))
end
(*let showBitvector (Bitvector elems start inc) =
@@ -410,6 +450,12 @@ let address_of_bitv v =
let bytes = bytes_of_bitv v in
address_of_byte_list bytes
+let rec reverse_endianness_bl bits =
+ if List.length bits <= 8 then bits else
+ list_append(reverse_endianness_bl(list_drop(8, bits)), list_take(8, bits))
+
+val reverse_endianness : forall 'a. Bitvector 'a => 'a -> 'a
+let reverse_endianness v = of_bits (reverse_endianness_bl (bits_of v))
(*** Registers *)
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 3cf017d1..edda208d 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1859,7 +1859,7 @@ let rewrite_guarded_clauses l cs =
let bitwise_and_exp exp1 exp2 =
let (E_aux (_,(l,_))) = exp1 in
- let andid = Id_aux (Id "bool_and", gen_loc l) in
+ let andid = Id_aux (Id "and_bool", gen_loc l) in
annot_exp (E_app(andid,[exp1;exp2])) l (env_of exp1) bool_typ
let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
@@ -2561,7 +2561,7 @@ let rewrite_constraint =
let rec rewrite_nc (NC_aux (nc_aux, l)) = mk_exp (rewrite_nc_aux nc_aux)
and rewrite_nc_aux = function
| NC_bounded_ge (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2))
- | NC_bounded_le (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2))
+ | NC_bounded_le (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "<=", mk_exp (E_sizeof n2))
| NC_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "==", mk_exp (E_sizeof n2))
| NC_not_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "!=", mk_exp (E_sizeof n2))
| NC_and (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "&", rewrite_nc nc2)
diff --git a/src/type_check.ml b/src/type_check.ml
index 3dd251ca..ff4a748b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2955,7 +2955,7 @@ and propagate_exp_effect_aux = function
| E_vector_subrange (v, i, j) ->
let p_v = propagate_exp_effect v in
let p_i = propagate_exp_effect i in
- let p_j = propagate_exp_effect i in
+ let p_j = propagate_exp_effect j in
E_vector_subrange (p_v, p_i, p_j), collect_effects [p_v; p_i; p_j]
| E_vector_update (v, i, x) ->
let p_v = propagate_exp_effect v in
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 16:36:12 +0000