From 92f50f2564834fcbeda250337c3acce571f7d6f0 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 16 Jul 2019 22:12:42 +0100 Subject: Fix all remaining tests for this branch --- aarch64/no_vector/spec.sail | 46 ++++++++++++++++++++++---------------------- aarch64/prelude.sail | 3 +-- aarch64_small/armV8.h.sail | 2 -- aarch64_small/prelude.sail | 7 ++----- lib/string.sail | 4 ++-- src/initial_check.ml | 1 - src/interpreter.ml | 19 ++++++++++++------ src/pretty_print_coq.ml | 41 ++++++++++++++++++++++++++------------- src/rewrites.ml | 2 +- src/value.ml | 5 +++++ test/builtins/unsigned1.sail | 2 +- test/builtins/unsigned3.sail | 2 +- test/builtins/unsigned7.sail | 2 +- test/builtins/unsigned8.sail | 2 +- 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 $include -// $include -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 $include $include 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 $include -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 $include -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 $include -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 $include -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 -- cgit v1.2.3