summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--aarch64/no_vector/spec.sail46
-rwxr-xr-xaarch64/prelude.sail3
-rw-r--r--aarch64_small/armV8.h.sail2
-rw-r--r--aarch64_small/prelude.sail7
-rw-r--r--lib/string.sail4
-rw-r--r--src/initial_check.ml1
-rw-r--r--src/interpreter.ml19
-rw-r--r--src/pretty_print_coq.ml41
-rw-r--r--src/rewrites.ml2
-rw-r--r--src/value.ml5
-rw-r--r--test/builtins/unsigned1.sail2
-rw-r--r--test/builtins/unsigned3.sail2
-rw-r--r--test/builtins/unsigned7.sail2
-rw-r--r--test/builtins/unsigned8.sail2
14 files changed, 79 insertions, 59 deletions
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail
index c91da297..149ddcd9 100644
--- a/aarch64/no_vector/spec.sail
+++ b/aarch64/no_vector/spec.sail
@@ -742,21 +742,21 @@ val __UNKNOWN_MemOp : unit -> MemOp
function __UNKNOWN_MemOp () = return(MemOp_LOAD)
-let MemHint_RWA : vector(2, dec, bit) = 0b11
+let MemHint_RWA : bits(2) = 0b11
-let MemHint_RA : vector(2, dec, bit) = 0b10
+let MemHint_RA : bits(2) = 0b10
-let MemHint_No : vector(2, dec, bit) = 0b00
+let MemHint_No : bits(2) = 0b00
val __UNKNOWN_MemBarrierOp : unit -> MemBarrierOp
function __UNKNOWN_MemBarrierOp () = return(MemBarrierOp_DSB)
-let MemAttr_WT : vector(2, dec, bit) = 0b10
+let MemAttr_WT : bits(2) = 0b10
-let MemAttr_WB : vector(2, dec, bit) = 0b11
+let MemAttr_WB : bits(2) = 0b11
-let MemAttr_NC : vector(2, dec, bit) = 0b00
+let MemAttr_NC : bits(2) = 0b00
val __UNKNOWN_MemAtomicOp : unit -> MemAtomicOp
@@ -782,23 +782,23 @@ register MAIR_EL2 : bits(64)
register MAIR_EL1 : bits(64)
-let M32_User : vector(5, dec, bit) = 0b10000
+let M32_User : bits(5) = 0b10000
-let M32_Undef : vector(5, dec, bit) = 0b11011
+let M32_Undef : bits(5) = 0b11011
-let M32_System : vector(5, dec, bit) = 0b11111
+let M32_System : bits(5) = 0b11111
-let M32_Svc : vector(5, dec, bit) = 0b10011
+let M32_Svc : bits(5) = 0b10011
-let M32_Monitor : vector(5, dec, bit) = 0b10110
+let M32_Monitor : bits(5) = 0b10110
-let M32_IRQ : vector(5, dec, bit) = 0b10010
+let M32_IRQ : bits(5) = 0b10010
-let M32_Hyp : vector(5, dec, bit) = 0b11010
+let M32_Hyp : bits(5) = 0b11010
-let M32_FIQ : vector(5, dec, bit) = 0b10001
+let M32_FIQ : bits(5) = 0b10001
-let M32_Abort : vector(5, dec, bit) = 0b10111
+let M32_Abort : bits(5) = 0b10111
val __UNKNOWN_LogicalOp : unit -> LogicalOp
@@ -1113,13 +1113,13 @@ register ELR_EL2 : bits(64)
register ELR_EL1 : bits(64)
-let EL3 : vector(2, dec, bit) = 0b11
+let EL3 : bits(2) = 0b11
-let EL2 : vector(2, dec, bit) = 0b10
+let EL2 : bits(2) = 0b10
-let EL1 : vector(2, dec, bit) = 0b01
+let EL1 : bits(2) = 0b01
-let EL0 : vector(2, dec, bit) = 0b00
+let EL0 : bits(2) = 0b00
register EDSCR : bits(32)
@@ -1149,13 +1149,13 @@ function DecodeRegExtend op = match op {
0b111 => return(ExtendType_SXTX)
}
-let DebugHalt_Watchpoint : vector(6, dec, bit) = 0b101011
+let DebugHalt_Watchpoint : bits(6) = 0b101011
-let DebugHalt_HaltInstruction : vector(6, dec, bit) = 0b101111
+let DebugHalt_HaltInstruction : bits(6) = 0b101111
-let DebugHalt_Breakpoint : vector(6, dec, bit) = 0b000111
+let DebugHalt_Breakpoint : bits(6) = 0b000111
-let DebugException_VectorCatch : vector(4, dec, bit) = 0x5
+let DebugException_VectorCatch : bits(4) = 0x5
val DataSynchronizationBarrier : (MBReqDomain, MBReqTypes) -> unit
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 21fcbe92..7bf0d9f9 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -2,9 +2,8 @@ default Order dec
$include <smt.sail>
$include <arith.sail>
-// $include <trace.sail>
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
val eq_vec = {ocaml: "eq_list", interpreter: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
diff --git a/aarch64_small/armV8.h.sail b/aarch64_small/armV8.h.sail
index d0f0b830..8b38f2eb 100644
--- a/aarch64_small/armV8.h.sail
+++ b/aarch64_small/armV8.h.sail
@@ -32,8 +32,6 @@
/* SUCH DAMAGE. */
/*========================================================================*/
-default Order dec
-
type boolean = bit
type integer = int
type uinteger = nat /* ARM ARM does not have nat/uint type */
diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail
index d94112ad..c904aec6 100644
--- a/aarch64_small/prelude.sail
+++ b/aarch64_small/prelude.sail
@@ -1,9 +1,8 @@
+default Order dec
+
let b1 = bitone
let b0 = bitzero
-
-/* default Order dec */
-
val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
/* sneaky deref with no effect necessary for bitfield writes */
val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
@@ -13,8 +12,6 @@ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
/* val eq_bit2 = "eq_bit" : (bit, bit) -> bool */
/* overload operator == = {eq_bit2} */
-
-
$include <smt.sail>
$include <flow.sail>
$include <arith.sail>
diff --git a/lib/string.sail b/lib/string.sail
index 120600ca..d5fe297e 100644
--- a/lib/string.sail
+++ b/lib/string.sail
@@ -15,9 +15,9 @@ val "dec_str" : int -> string
val "hex_str" : int -> string
-val bits_str = "string_of_bits" : forall 'n. vector('n, dec, bit) -> string
+val bits_str = "string_of_bits" : forall 'n. bitvector('n, dec) -> string
-val concat_str_bits : forall 'n. (string, vector('n, dec, bit)) -> string
+val concat_str_bits : forall 'n. (string, bitvector('n, dec)) -> string
function concat_str_bits(str, x) = concat_str(str, bits_str(x))
diff --git a/src/initial_check.ml b/src/initial_check.ml
index f41033ca..ec3e1f24 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -924,7 +924,6 @@ let undefined_builtin_val_specs =
extern_of_string (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
extern_of_string (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
- (* Only used with lem_mwords *)
extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> bitvector('n, dec) effect {undef}";
extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"]
diff --git a/src/interpreter.ml b/src/interpreter.ml
index def0963f..a2cc17bf 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -725,13 +725,20 @@ and pattern_match env (P_aux (p_aux, (l, _)) as pat) value =
recursive call that has an empty_tannot we must not use the
annotation in the whole vector_concat pattern. *)
let open Type_check in
+ let vector_concat_match n =
+ let init, rest = Util.take (Big_int.to_int n) (coerce_gv value), Util.drop (Big_int.to_int n) (coerce_gv value) in
+ let init_match, init_bind = pattern_match env pat (V_vector init) in
+ let rest_match, rest_bind = pattern_match env (P_aux (P_vector_concat pats, (l, empty_tannot))) (V_vector rest) in
+ init_match && rest_match, Bindings.merge combine init_bind rest_bind
+ in
begin match destruct_vector (env_of_pat pat) (typ_of_pat pat) with
- | Some (Nexp_aux (Nexp_constant n, _), _, _) ->
- let init, rest = Util.take (Big_int.to_int n) (coerce_gv value), Util.drop (Big_int.to_int n) (coerce_gv value) in
- let init_match, init_bind = pattern_match env pat (V_vector init) in
- let rest_match, rest_bind = pattern_match env (P_aux (P_vector_concat pats, (l, empty_tannot))) (V_vector rest) in
- init_match && rest_match, Bindings.merge combine init_bind rest_bind
- | _ -> failwith ("Bad vector annotation " ^ string_of_typ (Type_check.typ_of_pat pat))
+ | Some (Nexp_aux (Nexp_constant n, _), _, _) -> vector_concat_match n
+ | None ->
+ begin match destruct_bitvector (env_of_pat pat) (typ_of_pat pat) with
+ | Some (Nexp_aux (Nexp_constant n, _), _) -> vector_concat_match n
+ | _ -> failwith ("Bad bitvector annotation for bitvector concatenation pattern " ^ string_of_typ (Type_check.typ_of_pat pat))
+ end
+ | _ -> failwith ("Bad vector annotation for vector concatentation pattern " ^ string_of_typ (Type_check.typ_of_pat pat))
end
| P_tup [pat] -> pattern_match env pat value
| P_tup pats | P_list pats ->
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 1fea72ea..25abfed8 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -592,15 +592,18 @@ let rec doc_typ_fns ctx env =
parens (separate_map (space ^^ star ^^ space) (app_typ false) typs)
| _ -> app_typ atyp_needed ty
and app_typ atyp_needed ((Typ_aux (t, l)) as ty) = match t with
+ | Typ_app(Id_aux (Id "bitvector", _), [
+ A_aux (A_nexp m, _);
+ A_aux (A_order ord, _)]) ->
+ (* TODO: remove duplication with exists, below *)
+ let tpp = string "mword " ^^ doc_nexp ctx m in
+ if atyp_needed then parens tpp else tpp
| Typ_app(Id_aux (Id "vector", _), [
A_aux (A_nexp m, _);
A_aux (A_order ord, _);
A_aux (A_typ elem_typ, _)]) ->
(* TODO: remove duplication with exists, below *)
- let tpp = match elem_typ with
- | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> (* TODO: coq-compatible simplification *)
- string "mword " ^^ doc_nexp ctx m
- | _ -> string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ doc_nexp ctx m in
+ let tpp = string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ doc_nexp ctx m in
if atyp_needed then parens tpp else tpp
| Typ_app(Id_aux (Id "register", _), [A_aux (A_typ etyp, _)]) ->
let tpp = string "register_ref regstate register_value " ^^ typ etyp in
@@ -662,6 +665,23 @@ let rec doc_typ_fns ctx env =
braces (separate space [doc_var ctx var; colon; string "Z";
ampersand; doc_arithfact ctx env ~exists:(List.map kopt_kid kopts) nc])
end
+ | Typ_aux (Typ_app (Id_aux (Id "bitvector",_),
+ [A_aux (A_nexp m, _);
+ A_aux (A_order ord, _)]), _) ->
+ (* TODO: proper handling of m, complex elem type, dedup with above *)
+ let var = mk_kid "_vec" in (* TODO collision avoid *)
+ let kid_set = KidSet.of_list (List.map kopt_kid kopts) in
+ let m_pp = doc_nexp ctx ~skip_vars:kid_set m in
+ let tpp, len_pp = string "mword " ^^ m_pp, string "length_mword" in
+ let length_constraint_pp =
+ if KidSet.is_empty (KidSet.inter kid_set (nexp_frees m))
+ then None
+ else Some (separate space [len_pp; doc_var ctx var; equals; doc_nexp ctx m])
+ in
+ braces (separate space
+ [doc_var ctx var; colon; tpp;
+ ampersand;
+ doc_arithfact ctx env ~exists:(List.map kopt_kid kopts) ?extra:length_constraint_pp nc])
| Typ_aux (Typ_app (Id_aux (Id "vector",_),
[A_aux (A_nexp m, _);
A_aux (A_order ord, _);
@@ -670,11 +690,7 @@ let rec doc_typ_fns ctx env =
let var = mk_kid "_vec" in (* TODO collision avoid *)
let kid_set = KidSet.of_list (List.map kopt_kid kopts) in
let m_pp = doc_nexp ctx ~skip_vars:kid_set m in
- let tpp, len_pp = match elem_typ with
- | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) ->
- string "mword " ^^ m_pp, string "length_mword"
- | _ -> string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ m_pp,
- string "vec_length" in
+ let tpp, len_pp = string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ m_pp, string "vec_length" in
let length_constraint_pp =
if KidSet.is_empty (KidSet.inter kid_set (nexp_frees m))
then None
@@ -1020,9 +1036,8 @@ let rec typeclass_nexps (Typ_aux(t,l)) =
-> NexpSet.empty
| Typ_fn (t1,t2,_) -> List.fold_left NexpSet.union (typeclass_nexps t2) (List.map typeclass_nexps t1)
| Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts)
- | Typ_app (Id_aux (Id "vector",_),
- [A_aux (A_nexp size_nexp,_);
- _;A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)])
+ | Typ_app (Id_aux (Id "bitvector",_),
+ [A_aux (A_nexp size_nexp,_); _])
| Typ_app (Id_aux (Id "itself",_),
[A_aux (A_nexp size_nexp,_)]) ->
let size_nexp = nexp_simp size_nexp in
@@ -2020,7 +2035,7 @@ let doc_exp, doc_let =
| E_vector exps ->
let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
let start, (len, order, etyp) =
- if is_vector_typ t then vector_start_index t, vector_typ_args_of t
+ if is_vector_typ t || is_bitvector_typ t then vector_start_index t, vector_typ_args_of t
else raise (Reporting.err_unreachable l __POS__
"E_vector of non-vector type") in
let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 0f747f59..3012e49b 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2099,7 +2099,7 @@ let rewrite_vector_concat_assignments env defs =
let (_, ord, etyp) = vector_typ_args_of typ in
let len (LEXP_aux (le, lannot)) =
let ltyp = Env.base_typ_of env (typ_of_annot lannot) in
- if is_vector_typ ltyp then
+ if is_vector_typ ltyp || is_bitvector_typ ltyp then
let (len, _, _) = vector_typ_args_of ltyp in
match nexp_simp len with
| Nexp_aux (Nexp_constant len, _) -> len
diff --git a/src/value.ml b/src/value.ml
index c509c81f..71d9ffe6 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -483,6 +483,10 @@ let value_undefined_vector = function
| [v1; v2] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, v2))
| _ -> failwith "value undefined_vector"
+let value_undefined_bitvector = function
+ | [v] -> V_vector (Sail_lib.undefined_vector (coerce_int v, V_bit (Sail_lib.B0)))
+ | _ -> failwith "value undefined_bitvector"
+
let value_read_ram = function
| [v1; v2; v3; v4] -> mk_vector (Sail_lib.read_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4))
| _ -> failwith "value read_ram"
@@ -731,6 +735,7 @@ let primops =
("undefined_int", fun _ -> V_int Big_int.zero);
("undefined_nat", fun _ -> V_int Big_int.zero);
("undefined_bool", fun _ -> V_bool false);
+ ("undefined_bitvector", value_undefined_bitvector);
("undefined_vector", value_undefined_vector);
("undefined_string", fun _ -> V_string "");
("internal_pick", value_internal_pick);
diff --git a/test/builtins/unsigned1.sail b/test/builtins/unsigned1.sail
index 15403598..8ef872c3 100644
--- a/test/builtins/unsigned1.sail
+++ b/test/builtins/unsigned1.sail
@@ -3,7 +3,7 @@ default Order dec
$include <exception_basic.sail>
$include <vector_dec.sail>
-val flip_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (vector('v, dec, bit), atom('len)) -> vector('len, dec, bit)
+val flip_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (bitvector('v, dec), atom('len)) -> bitvector('len, dec)
function flip_mask(v, len) = len ^ v
diff --git a/test/builtins/unsigned3.sail b/test/builtins/unsigned3.sail
index e318dfdd..73bfb31d 100644
--- a/test/builtins/unsigned3.sail
+++ b/test/builtins/unsigned3.sail
@@ -3,7 +3,7 @@ default Order dec
$include <exception_basic.sail>
$include <vector_dec.sail>
-val flip_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (vector('v, dec, bit), atom('len)) -> vector('len, dec, bit)
+val flip_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (bitvector('v, dec), atom('len)) -> bitvector('len, dec)
function flip_mask(v, len) = len ^ v
diff --git a/test/builtins/unsigned7.sail b/test/builtins/unsigned7.sail
index 466c1701..fac71139 100644
--- a/test/builtins/unsigned7.sail
+++ b/test/builtins/unsigned7.sail
@@ -3,7 +3,7 @@ default Order dec
$include <exception_basic.sail>
$include <vector_dec.sail>
-val flip_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (vector('v, dec, bit), atom('len)) -> vector('len, dec, bit)
+val flip_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (bitvector('v, dec), atom('len)) -> bitvector('len, dec)
function flip_mask(v, len) = len ^ v
diff --git a/test/builtins/unsigned8.sail b/test/builtins/unsigned8.sail
index 58302622..3bd9da82 100644
--- a/test/builtins/unsigned8.sail
+++ b/test/builtins/unsigned8.sail
@@ -3,7 +3,7 @@ default Order dec
$include <exception_basic.sail>
$include <vector_dec.sail>
-val flip_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (vector('v, dec, bit), atom('len)) -> vector('len, dec, bit)
+val flip_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (bitvector('v, dec), atom('len)) -> bitvector('len, dec)
function flip_mask(v, len) = len ^ v
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:42:24 +0000