diff options
| -rw-r--r-- | isabelle-lib/Makefile | 4 | ||||
| -rw-r--r-- | mips/mips_extras_embed_sequential.lem | 30 | ||||
| -rw-r--r-- | src/gen_lib/prompt.lem | 4 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 53 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 72 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 280 | ||||
| -rw-r--r-- | src/pretty_print_ocaml.ml | 6 | ||||
| -rw-r--r-- | src/type_internal.ml | 38 | ||||
| -rw-r--r-- | src/type_internal.mli | 3 |
9 files changed, 335 insertions, 155 deletions
diff --git a/isabelle-lib/Makefile b/isabelle-lib/Makefile index bd4066cd..11cdbc27 100644 --- a/isabelle-lib/Makefile +++ b/isabelle-lib/Makefile @@ -37,5 +37,5 @@ prompt.lem: ../src/gen_lib/prompt.lem cp $< . clean: - rm $(THYS) $(LEMS) - rm *Auxiliary.thy + -rm $(THYS) $(LEMS) + -rm *Auxiliary.thy diff --git a/mips/mips_extras_embed_sequential.lem b/mips/mips_extras_embed_sequential.lem index 73dc42ed..708c1f63 100644 --- a/mips/mips_extras_embed_sequential.lem +++ b/mips/mips_extras_embed_sequential.lem @@ -4,10 +4,10 @@ open import Sail_impl_base open import Sail_values open import State -val MEMr : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserve : (vector bitU * integer) -> M (vector bitU) -val MEMr_tag : (vector bitU * integer) -> M (bitU * vector bitU) -val MEMr_tag_reserve : (vector bitU * integer) -> M (bitU * vector bitU) +val MEMr : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitvector 'b) +val MEMr_reserve : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitvector 'b) +val MEMr_tag : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitU * bitvector 'b) +val MEMr_tag_reserve : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitU * bitvector 'b) let MEMr (addr,size) = read_mem false Read_plain addr size let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size @@ -23,10 +23,10 @@ let MEMr_tag_reserve (addr,size) = return (t, v) -val MEMea : (vector bitU * integer) -> M unit -val MEMea_conditional : (vector bitU * integer) -> M unit -val MEMea_tag : (vector bitU * integer) -> M unit -val MEMea_tag_conditional : (vector bitU * integer) -> M unit +val MEMea : forall 'a. (bitvector 'a * integer) -> M unit +val MEMea_conditional : forall 'a. (bitvector 'a * integer) -> M unit +val MEMea_tag : forall 'a. (bitvector 'a * integer) -> M unit +val MEMea_tag_conditional : forall 'a. (bitvector 'a * integer) -> M unit let MEMea (addr,size) = write_mem_ea Write_plain addr size let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size @@ -35,10 +35,10 @@ let MEMea_tag (addr,size) = write_mem_ea Write_plain addr size let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size -val MEMval : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU -val MEMval_tag : (vector bitU * integer * bitU * vector bitU) -> M unit -val MEMval_tag_conditional : (vector bitU * integer * bitU * vector bitU) -> M bitU +val MEMval : forall 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M unit +val MEMval_conditional : forall 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M bitU +val MEMval_tag : forall 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M unit +val MEMval_tag_conditional : forall 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M bitU let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) @@ -50,7 +50,9 @@ val MEM_sync : unit -> M unit let MEM_sync () = barrier Barrier_MIPS_SYNC +(* TODO: Consider moving this to sail_values.lem (after fixing and implementing + a default index ordering) *) let duplicate (bit,len) = - let bits = repeat [bit] len in + let bits = repeat [bitU_to_bool bit] len in let start = len - 1 in - Vector bits start false + Bitvector (wordFromBitlist bits) start false diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 426b0811..70850dc1 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -71,12 +71,12 @@ let read_reg_range reg i j = read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) let read_reg_bit reg i = read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v -> - return (extract_only_bit v) + return (extract_only_element v) let read_reg_field reg regfield = read_reg_aux (external_reg_field_whole reg regfield) let read_reg_bitfield reg regfield = read_reg_aux (external_reg_field_whole reg regfield) >>= fun v -> - return (extract_only_bit v) + return (extract_only_element v) val write_reg_aux : reg_name -> vector bitU -> M unit let write_reg_aux reg_name v = diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index ecfd3ce7..bccdd8f2 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -218,6 +218,14 @@ instance forall 'a. Show 'a => (Show (bitvector 'a)) let show = showBitvector end +let bvec_to_vec (Bitvector bs start is_inc) = + let bits = List.map bool_to_bitU (bitlistFromWord bs) in + Vector bits start is_inc + +let vec_to_bvec (Vector elems start is_inc) = + let word = wordFromBitlist (List.map bitU_to_bool elems) in + Bitvector word start is_inc + (*** Vector operations *) val set_bitvector_start : forall 'a. integer -> bitvector 'a -> bitvector 'a @@ -265,7 +273,7 @@ let bvupdate_aux (Bitvector bs start is_inc) i j bs' = let bits = word_update bs lo hi bs' in Bitvector bits start is_inc -val bvupdate : forall 'a. bitvector 'a -> integer -> integer -> bitvector 'a -> bitvector 'a +val bvupdate : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a let bvupdate v i j (Bitvector bs' _ _) = bvupdate_aux v i j bs' @@ -273,25 +281,32 @@ let bvupdate v i j (Bitvector bs' _ _) = val getBit' : forall 'a. mword 'a -> nat -> bool let getBit' w n = getBit w (naturalFromNat n) -val bvaccess : forall 'a. bitvector 'a -> integer -> bool -let bvaccess (Bitvector bs start is_inc) n = +val bvaccess : forall 'a. bitvector 'a -> integer -> bitU +let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU ( if is_inc then getBit' bs (natFromInteger (n - start)) - else getBit' bs (natFromInteger (start - n)) + else getBit' bs (natFromInteger (start - n))) -val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bool -> bitvector 'a +val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bitU -> bitvector 'a let bvupdate_pos v n b = - bvupdate_aux v n n ((wordFromNatural (if b then 1 else 0)) : mword ty1) + bvupdate_aux v n n ((wordFromNatural (if bitU_to_bool b then 1 else 0)) : mword ty1) (*** Bit vector operations *) +let extract_only_element (Vector elems _ _) = match elems with + | [] -> failwith "extract_only_element called for empty vector" + | [e] -> e + | _ -> failwith "extract_only_element called for vector with more elements" +end + +val extract_only_bit : bitvector ty1 -> bitU let extract_only_bit (Bitvector elems _ _) = - let l = word_length elems in - if l = 1 then - msb elems - else if l = 0 then + (*let l = word_length elems in + if l = 1 then*) + bool_to_bitU (msb elems) + (*else if l = 0 then failwith "extract_single_bit called for empty vector" else - failwith "extract_single_bit called for vector with more bits" + failwith "extract_single_bit called for vector with more bits"*) let pp_bitu_vector (Vector elems start inc) = let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in @@ -302,7 +317,7 @@ let most_significant (Bitvector v _ _) = if word_length v = 0 then failwith "most_significant applied to empty vector" else - msb v + bool_to_bitU (msb v) let bitwise_not_bitlist = List.map bitwise_not_bit @@ -402,13 +417,14 @@ let to_vec_big = to_vec let to_vec_inc = to_vec true let to_vec_dec = to_vec false -(* TODO?? + +(* TODO: Think about undefined bit(vector)s *) let to_vec_undef is_inc (len : integer) = - Vector (replicate (natFromInteger len) BU) (if is_inc then 0 else len-1) is_inc + Bitvector (failwith "undefined bitvector") (if is_inc then 0 else len-1) is_inc let to_vec_inc_undef = to_vec_undef true let to_vec_dec_undef = to_vec_undef false -*) + let exts (len, vec) = to_vec (bvget_dir vec) (len,signed vec) let extz (len, vec) = to_vec (bvget_dir vec) (len,unsigned vec) @@ -737,9 +753,9 @@ let make_bitvector_undef length = (* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *) -let mask (n,Vector bits start dir) = - let current_size = List.length bits in - Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir +let mask (n,bv) = + let len = bvlength bv in + bvslice_raw bv (len - n) (len - 1) val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a) @@ -1026,4 +1042,3 @@ let diafp_to_dia reginfo = function | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v) | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r) end - diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 430ee562..709052fe 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -47,12 +47,12 @@ let set_reg state reg bitv = <| state with regstate = Map.insert reg bitv state.regstate |> -val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU) +val read_mem : forall 'a 'b. Size 'b => bool -> read_kind -> bitvector 'a -> integer -> M (bitvector 'b) let read_mem dir read_kind addr sz state = - let addr = integer_of_address (address_of_bitv addr) in + let addr = unsigned addr in let addrs = range addr (addr+sz-1) in let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in - let value = Sail_values.internal_mem_value dir memory_value in + let value = vec_to_bvec (Sail_values.internal_mem_value dir memory_value) in let is_exclusive = match read_kind with | Sail_impl_base.Read_plain -> false | Sail_impl_base.Read_reserve -> true @@ -69,9 +69,9 @@ let read_mem dir read_kind addr sz state = (* caps are aligned at 32 bytes *) let cap_alignment = (32 : integer) -val read_tag : bool -> read_kind -> vector bitU -> M bitU +val read_tag : forall 'a. bool -> read_kind -> bitvector 'a -> M bitU let read_tag dir read_kind addr state = - let addr = (integer_of_address (address_of_bitv addr)) / cap_alignment in + let addr = (unsigned addr) / cap_alignment in let tag = match (Map.lookup addr state.tagstate) with | Just t -> t | Nothing -> B0 @@ -96,18 +96,18 @@ let excl_result () state = (Left true, <| state with last_exclusive_operation_was_load = false |>) in (Left false, state) :: if state.last_exclusive_operation_was_load then [success] else [] -val write_mem_ea : write_kind -> vector bitU -> integer -> M unit +val write_mem_ea : forall 'a. write_kind -> bitvector 'a -> integer -> M unit let write_mem_ea write_kind addr sz state = - let addr = integer_of_address (address_of_bitv addr) in + let addr = unsigned addr in [(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)] -val write_mem_val : vector bitU -> M bool +val write_mem_val : forall 'b. bitvector 'b -> M bool let write_mem_val v state = let (write_kind,addr,sz) = match state.write_ea with | Nothing -> failwith "write ea has not been announced yet" | Just write_ea -> write_ea end in let addrs = range addr (addr+sz-1) in - let v = external_mem_value v in + let v = external_mem_value (bvec_to_vec v) in let addresses_with_value = List.zip addrs v in let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem) state.memstate addresses_with_value in @@ -122,16 +122,16 @@ let write_tag t state = let tagstate = Map.insert taddr t state.tagstate in [(Left true, <| state with tagstate = tagstate |>)] -val read_reg : register -> M (vector bitU) +val read_reg : forall 'a. Size 'a => register -> M (bitvector 'a) let read_reg reg state = - let v = Map_extra.find (name_of_reg reg) state.regstate in + let v = get_reg state (name_of_reg reg) in + [(Left (vec_to_bvec v),state)] +let read_reg_range reg i j state = + let v = slice (get_reg state (name_of_reg reg)) i j in + [(Left (vec_to_bvec v),state)] +let read_reg_bit reg i state = + let v = access (get_reg state (name_of_reg reg)) i in [(Left v,state)] -let read_reg_range reg i j = - read_reg reg >>= fun rv -> - return (slice rv i j) -let read_reg_bit reg i = - read_reg_range reg i i >>= fun v -> - return (extract_only_bit v) let read_reg_field reg regfield = let (i,j) = register_field_indices reg regfield in read_reg_range reg i j @@ -139,25 +139,30 @@ let read_reg_bitfield reg regfield = let (i,_) = register_field_indices reg regfield in read_reg_bit reg i -val write_reg : register -> vector bitU -> M unit +val write_reg : forall 'a. Size 'a => register -> bitvector 'a -> M unit let write_reg reg v state = - [(Left (),<| state with regstate = Map.insert (name_of_reg reg) v state.regstate |>)] -let write_reg_range reg i j v = - read_reg reg >>= fun current_value -> - let new_value = update current_value i j v in - write_reg reg new_value -let write_reg_bit reg i bit = - write_reg_range reg i i (Vector [bit] i (is_inc_of_reg reg)) + [(Left (), set_reg state (name_of_reg reg) (bvec_to_vec v))] +let write_reg_range reg i j v state = + let current_value = get_reg state (name_of_reg reg) in + let new_value = update current_value i j (bvec_to_vec v) in + [(Left (), set_reg state (name_of_reg reg) new_value)] +let write_reg_bit reg i bit state = + let current_value = get_reg state (name_of_reg reg) in + let new_value = update_pos current_value i bit in + [(Left (), set_reg state (name_of_reg reg) new_value)] let write_reg_field reg regfield = - let (i,j) = register_field_indices reg regfield in + let (i,j) = register_field_indices reg regfield in write_reg_range reg i j let write_reg_bitfield reg regfield = let (i,_) = register_field_indices reg regfield in write_reg_bit reg i -let write_reg_field_range reg regfield i j v = - read_reg_field reg regfield >>= fun current_field_value -> - let new_field_value = update current_field_value i j v in - write_reg_field reg regfield new_field_value +let write_reg_field_range reg regfield i j v state = + let (i0,j0) = register_field_indices reg regfield in + let current_value = get_reg state (name_of_reg reg) in + let current_field_value = slice current_value i0 j0 in + let new_field_value = update current_field_value i j (bvec_to_vec v) in + let new_value = update current_value i j new_field_value in + [(Left (), set_reg state (name_of_reg reg) new_value)] val barrier : barrier_kind -> M unit @@ -186,7 +191,8 @@ let rec foreachM_dec (i,stop,by) vars body = foreachM_dec (i - by,stop,by) vars body else return vars -let write_two_regs r1 r2 vec = +let write_two_regs r1 r2 bvec state = + let vec = bvec_to_vec bvec in let is_inc = let is_inc_r1 = is_inc_of_reg r1 in let is_inc_r2 = is_inc_of_reg r2 in @@ -205,4 +211,6 @@ let write_two_regs r1 r2 vec = if is_inc then slice vec (size_r1 - start_vec) (size_vec - start_vec) else slice vec (start_vec - size_r1) (start_vec - size_vec) in - write_reg r1 r1_v >> write_reg r2 r2_v + let state1 = set_reg state (name_of_reg r1) r1_v in + let state2 = set_reg state1 (name_of_reg r2) r2_v in + [(Left (), state2)] diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 65c679ff..5f2e9888 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -118,18 +118,24 @@ let doc_id_lem_ctor (Id_aux(i,_)) = * token in case of x ending with star. *) separate space [colon; string (String.capitalize x); empty] +let effectful_set = + List.exists + (fun (BE_aux (eff,_)) -> + match eff with + | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem + | BE_exmem | BE_wmv | BE_wmvt | BE_barr | BE_depend | BE_nondet + | BE_escape -> true + | _ -> false) + let effectful (Effect_aux (eff,_)) = match eff with | Effect_var _ -> failwith "effectful: Effect_var not supported" - | Effect_set effs -> - List.exists - (fun (BE_aux (eff,_)) -> - match eff with - | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem - | BE_exmem | BE_wmv | BE_wmvt | BE_barr | BE_depend | BE_nondet - | BE_escape -> true - | _ -> false) - effs + | Effect_set effs -> effectful_set effs + +let effectful_t eff = + match eff.effect with + | Eset effs -> effectful_set effs + | _ -> false let rec is_number {t=t} = match t with @@ -166,9 +172,20 @@ let doc_typ_lem, doc_atomic_typ_lem = Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) -> let tpp = match elem_typ with - | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> string "bitvector" ^^ space ^^ doc_nexp m + | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> + let len = match m with + | (Nexp_aux(Nexp_constant i,_)) -> string "ty" ^^ doc_int i + | _ -> doc_nexp m in + string "bitvector" ^^ space ^^ len | _ -> string "vector" ^^ space ^^ typ regtypes elem_typ in if atyp_needed then parens tpp else tpp + | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> + (* TODO: Better distinguish register names and contents? + The former are represented in the Lem library using a type + "register" (without parameters), the latter just using the content + type (e.g. "bitvector ty64"). We assume the latter is meant here + and drop the "register" keyword. *) + fn_typ regtypes atyp_needed etyp | Typ_app(Id_aux (Id "range", _),_) -> (string "integer") | Typ_app(Id_aux (Id "implicit", _),_) -> @@ -195,12 +212,17 @@ let doc_typ_lem, doc_atomic_typ_lem = let tpp = typ regtypes ty in if atyp_needed then parens tpp else tpp and doc_typ_arg_lem regtypes (Typ_arg_aux(t,_)) = match t with - | Typ_arg_typ t -> app_typ regtypes false t + | Typ_arg_typ t -> app_typ regtypes true t | Typ_arg_nexp n -> empty | Typ_arg_order o -> empty | Typ_arg_effect e -> empty in typ', atomic_typ +let doc_tannot_lem regtypes eff t = + let ta = doc_typ_lem regtypes (t_to_typ (normalize_t t)) in + if eff then string " : M " ^^ parens ta + else string " : " ^^ ta + (* doc_lit_lem gets as an additional parameter the type information from the * expression around it: that's a hack, but how else can we distinguish between * undefined values of different types ? *) @@ -276,6 +298,44 @@ let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p w | _ -> parens (separate_map comma_sp (doc_pat_lem regtypes false) pats)) | P_list pats -> brackets (separate_map semi (doc_pat_lem regtypes false) pats) (*Never seen but easy in lem*) +let rec contains_bitvector_type t = match t.t with + | Ttup ts -> List.exists contains_bitvector_type ts + | Tapp (_, targs) -> is_bit_vector t || List.exists contains_bitvector_type_arg targs + | Tabbrev (_,t') -> contains_bitvector_type t' + | Tfn (t1,t2,_,_) -> contains_bitvector_type t1 || contains_bitvector_type t2 + | _ -> false +and contains_bitvector_type_arg targ = match targ with + | TA_typ t -> contains_bitvector_type t + | _ -> false + +let const_nexp nexp = match nexp.nexp with + | Nconst _ -> true + | _ -> false + +(* Check for variables in types that would be pretty-printed. + In particular, in case of vector types, only the element type and the + length argument are checked for variables, and the latter only if it is + a bitvector; for other types of vectors, the length is not pretty-printed + in the type, and the start index is never pretty-printed in vector types. *) +let rec contains_t_pp_var t = match t.t with + | Tvar _ -> true + | Tfn (t1,t2,_,_) -> contains_t_pp_var t1 || contains_t_pp_var t2 + | Ttup ts -> List.exists contains_t_pp_var ts + | Tapp ("vector",[_;TA_nexp m;_;TA_typ t']) -> + if is_bit_vector t then not (const_nexp (normalize_nexp m)) + else contains_t_pp_var t' + | Tapp (c,targs) -> List.exists contains_t_arg_pp_var targs + | Tabbrev (_,t') -> contains_t_pp_var t' + | Toptions (t1,t2o) -> + contains_t_pp_var t1 || + (match t2o with Some t2 -> contains_t_pp_var t2 | _ -> false) + | Tuvar _ -> true + | Tid _ -> false +and contains_t_arg_pp_var targ = match targ with + | TA_typ t -> contains_t_pp_var t + | TA_nexp nexp -> not (const_nexp (normalize_nexp nexp)) + | _ -> false + let prefix_recordtype = true let report = Reporting_basic.err_unreachable let doc_exp_lem, doc_let_lem = @@ -342,8 +402,15 @@ let doc_exp_lem, doc_let_lem = | _ -> (prefix 2 1) (string "write_reg") (doc_lexp_deref_lem regtypes le ^/^ expY e)) | E_vector_append(l,r) -> + let (Base((_,t),_,_,_,_,_)) = annot in + let (call,ta,aexp_needed) = + if is_bit_vector t then + if not (contains_t_pp_var t) + then ("bitvector_concat", doc_tannot_lem regtypes false t, true) + else ("bitvector_concat", empty, aexp_needed) + else ("vector_concat",empty,aexp_needed) in let epp = - align (group (separate space [expY l;string "^^"] ^/^ expY r)) in + align (group (separate space [string call;expY l;expY r])) ^^ ta in if aexp_needed then parens epp else epp | E_cons(l,r) -> doc_op (group (colon^^colon)) (expY l) (expY r) | E_if(c,t,e) -> @@ -388,7 +455,15 @@ let doc_exp_lem, doc_let_lem = if aexp_needed then parens (align epp) else epp | Id_aux (Id "slice_raw",_) -> let [e1;e2;e3] = args in - let epp = separate space [string "slice_raw";expY e1;expY e2;expY e3] in + let (E_aux (_,(_,Base((_,t1),_,_,_,_,_)))) = e1 in + let call = if is_bit_vector t1 then "bvslice_raw" else "slice_raw" in + let epp = separate space [string call;expY e1;expY e2;expY e3] in + if aexp_needed then parens (align epp) else epp + | Id_aux (Id "length",_) -> + let [arg] = args in + let (E_aux (_,(_,Base((_,targ),_,_,_,_,_)))) = arg in + let call = if is_bit_vector targ then "bvlength" else "length" in + let epp = separate space [string call;expY arg] in if aexp_needed then parens (align epp) else epp | _ -> begin match annot with @@ -398,10 +473,13 @@ let doc_exp_lem, doc_let_lem = if aexp_needed then parens (align epp) else epp | Base (_,Constructor _,_,_,_,_) -> let argpp a_needed arg = - let (E_aux (_,(_,Base((_,{t=t}),_,_,_,_,_)))) = arg in - match t with - | Tapp("vector",_) -> - let epp = concat [string "reset_vector_start";space;expY arg] in + let (E_aux (_,(_,Base((_,t),_,_,_,_,_)))) = arg in + match t.t with + | Tapp("vector",[_;_;_;_]) -> + let call = + if is_bit_vector t then "reset_bitvector_start" + else "reset_vector_start" in + let epp = concat [string call;space;expY arg] in if a_needed then parens epp else epp | _ -> expV a_needed arg in let epp = @@ -417,17 +495,25 @@ let doc_exp_lem, doc_let_lem = | Base(_,External (Some n),_,_,_,_) -> string n | _ -> doc_id_lem f in let argpp a_needed arg = - let (E_aux (_,(_,Base((_,{t=t}),_,_,_,_,_)))) = arg in - match t with - | Tapp("vector",_) -> - let epp = concat [string "reset_vector_start";space;expY arg] in + let (E_aux (_,(_,Base((_,t),_,_,_,_,_)))) = arg in + match t.t with + | Tapp("vector",[_;_;_;_]) -> + let call = + if is_bit_vector t then "reset_bitvector_start" + else "reset_vector_start" in + let epp = concat [string call;space;expY arg] in if a_needed then parens epp else epp | _ -> expV a_needed arg in let argspp = match args with | [arg] -> argpp true arg | args -> parens (align (separate_map (comma ^^ break 0) (argpp false) args)) in let epp = align (call ^//^ argspp) in - if aexp_needed then parens (align epp) else epp + let (taepp,aexp_needed) = + let (Base ((_,t),_,_,eff,_,_)) = annot in + if contains_bitvector_type t && not (contains_t_pp_var t) + then (align epp ^^ (doc_tannot_lem regtypes (effectful_t eff) t), true) + else (epp, aexp_needed) in + if aexp_needed then parens (align taepp) else taepp end end | E_vector_access (v,e) -> @@ -436,27 +522,40 @@ let doc_exp_lem, doc_let_lem = if has_rreg_effect eff then separate space [string "read_reg_bit";expY v;expY e] else - separate space [string "access";expY v;expY e] in + let (E_aux (_,(_,Base ((_,tv),_,_,_,_,_)))) = v in + let call = if is_bit_vector tv then "bvaccess" else "access" in + separate space [string call;expY v;expY e] in if aexp_needed then parens (align epp) else epp | E_vector_subrange (v,e1,e2) -> - let (Base (_,_,_,_,eff,_)) = annot in - let epp = + let (Base ((_,t),_,_,_,eff,_)) = annot in + let (epp,aexp_needed) = if has_rreg_effect eff then - align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) + let epp = align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in + if contains_bitvector_type t && not (contains_t_pp_var t) + then (epp ^^ doc_tannot_lem regtypes true t, true) + else (epp, aexp_needed) else - align (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in + if is_bit_vector t then + let bepp = string "bvslice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2 in + if not (contains_t_pp_var t) + then (bepp ^^ doc_tannot_lem regtypes false t, true) + else (bepp, aexp_needed) + else (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2, aexp_needed) in if aexp_needed then parens (align epp) else epp | E_field((E_aux(_,(l,fannot)) as fexp),id) -> - let (Base ((_,{t = t}),_,_,_,_,_)) = fannot in - (match t with + let (Base ((_,{t = ft}),_,_,_,_,_)) = fannot in + (match ft with | Tabbrev({t = Tid regtyp},{t=Tapp("register",_)}) -> - let field_f = match annot with - | Base((_,{t = Tid "bit"}),_,_,_,_,_) - | Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) -> - string "read_reg_bitfield" + let (Base((_,t),_,_,_,_,_)) = annot in + let field_f = match t.t with + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> string "read_reg_bitfield" | _ -> string "read_reg_field" in + let (ta,aexp_needed) = + if contains_bitvector_type t && not (contains_t_pp_var t) + then (doc_tannot_lem regtypes true t, true) + else (empty, aexp_needed) in let epp = field_f ^^ space ^^ (expY fexp) ^^ space ^^ string_lit (doc_id_lem id) in - if aexp_needed then parens (align epp) else epp + if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta) | Tid recordtyp | Tabbrev ({t = Tid recordtyp},_) -> let fname = @@ -470,57 +569,73 @@ let doc_exp_lem, doc_let_lem = | E_block exps -> raise (report l "Blocks should have been removed till now.") | E_nondet exps -> raise (report l "Nondet blocks not supported.") | E_id id -> + let (Base((_,t),_,_,_,_,_)) = annot in (match annot with | Base((_, ({t = Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})), External _,_,eff,_,_) -> if has_rreg_effect eff then - separate space [string "read_reg";doc_id_lem id] + let epp = separate space [string "read_reg";doc_id_lem id] in + if contains_bitvector_type t && not (contains_t_pp_var t) + then parens (epp ^^ doc_tannot_lem regtypes true t) + else epp else doc_id_lem id | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_lem_ctor id | Base((_,t),Alias alias_info,_,eff,_,_) -> (match alias_info with | Alias_field(reg,field) -> - let epp = match t.t with - | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> - (separate space) - [string "read_reg_bitfield"; string reg;string_lit(string field)] - | _ -> - (separate space) - [string "read_reg_field"; string reg; string_lit(string field)] in - if aexp_needed then parens (align epp) else epp + let call = match t.t with + | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> "read_reg_bitfield" + | _ -> "read_reg_field" in + let ta = + if contains_bitvector_type t && not (contains_t_pp_var t) + then doc_tannot_lem regtypes true t else empty in + let epp = separate space [string call;string reg;string_lit(string field)] ^^ ta in + if aexp_needed then parens (align epp) else epp | Alias_pair(reg1,reg2) -> - let epp = - if has_rreg_effect eff then - separate space [string "read_two_regs";string reg1;string reg2] - else - separate space [string "RegisterPair";string reg1;string reg2] in - if aexp_needed then parens (align epp) else epp + let (call,ta) = + if has_rreg_effect eff then + let ta = + if contains_bitvector_type t && not (contains_t_pp_var t) + then doc_tannot_lem regtypes true t else empty in + ("read_two_regs", ta) + else + ("RegisterPair", empty) in + let epp = separate space [string call;string reg1;string reg2] ^^ ta in + if aexp_needed then parens (align epp) else epp | Alias_extract(reg,start,stop) -> - let epp = - if start = stop then - (separate space) - [string "access";doc_int start; - parens (string "read_reg" ^^ space ^^ string reg)] - else - (separate space) - [string "slice"; doc_int start; doc_int stop; - parens (string "read_reg" ^^ space ^^ string reg)] in - if aexp_needed then parens (align epp) else epp + let epp = + if start = stop then + separate space [string "read_reg_bit";string reg;doc_int start] + else + let ta = + if contains_bitvector_type t && not (contains_t_pp_var t) + then doc_tannot_lem regtypes true t else empty in + separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in + if aexp_needed then parens (align epp) else epp ) | _ -> doc_id_lem id) | E_lit lit -> doc_lit_lem false lit annot | E_cast(Typ_aux (typ,_),e) -> (match annot with - | Base(_,External _,_,_,_,_) -> string "read_reg" ^^ space ^^ expY e - | _ -> + | Base((_,t),External _,_,_,_,_) -> + let epp = string "read_reg" ^^ space ^^ expY e in + if contains_bitvector_type t && not (contains_t_pp_var t) + then parens (epp ^^ doc_tannot_lem regtypes true t) else epp + | Base((_,t),_,_,_,_,_) -> (match typ with | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) -> - let epp = (concat [string "set_vector_start";space;string (string_of_int i)]) ^//^ + let call = + if is_bit_vector t then "set_bitvector_start" + else "set_vector_start" in + let epp = (concat [string call;space;string (string_of_int i)]) ^//^ expY e in if aexp_needed then parens epp else epp | Typ_var (Kid_aux (Var "length",_)) -> - let epp = (string "set_vector_start_to_length") ^//^ expY e in + let call = + if is_bit_vector t then "set_bitvector_start_to_length" + else "set_vector_start_to_length" in + let epp = (string call) ^//^ expY e in if aexp_needed then parens epp else epp | _ -> expV aexp_needed e)) (*(parens (doc_op colon (group (expY e)) (doc_typ_lem typ)))) *) @@ -549,8 +664,8 @@ let doc_exp_lem, doc_let_lem = (match annot with | Base((_,t),_,_,_,_,_) -> match t.t with - | Tapp("vector", [TA_nexp start; _; TA_ord order; _]) - | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; _; TA_ord order; _])}) -> + | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp]) + | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])}) -> let dir,dir_out = match order.order with | Oinc -> true,"true" | _ -> false, "false" in @@ -572,6 +687,13 @@ let doc_exp_lem, doc_let_lem = align (group expspp) in let epp = group (separate space [string "Vector"; brackets expspp;string start;string dir_out]) in + let (epp,aexp_needed) = + if etyp.t = Tid "bit" then + let bepp = string "vec_to_bvec" ^^ space ^^ parens (align epp) in + if contains_t_pp_var t + then (bepp, aexp_needed) + else (bepp ^^ doc_tannot_lem regtypes false t, true) + else (epp,aexp_needed) in if aexp_needed then parens (align epp) else epp ) | E_vector_indexed (iexps, (Def_val_aux (default,(dl,dannot)))) -> @@ -627,12 +749,20 @@ let doc_exp_lem, doc_let_lem = let epp = align (group (call ^//^ brackets expspp ^/^ separate space [default_string;string start;string size;string dir_out])) in - if aexp_needed then parens (align epp) else epp + let (bepp, aexp_needed) = + if is_bit_vector t + then (string "vec_to_bvec" ^^ space ^^ parens (epp) ^^ doc_tannot_lem regtypes false t, true) + else (epp, aexp_needed) in + if aexp_needed then parens (align bepp) else bepp | E_vector_update(v,e1,e2) -> - let epp = separate space [string "update_pos";expY v;expY e1;expY e2] in + let (Base((_,t),_,_,_,_,_)) = annot in + let call = if is_bit_vector t then "bvupdate_pos" else "update_pos" in + let epp = separate space [string call;expY v;expY e1;expY e2] in if aexp_needed then parens (align epp) else epp | E_vector_update_subrange(v,e1,e2,e3) -> - let epp = align (string "update" ^//^ + let (Base((_,t),_,_,_,_,_)) = annot in + let call = if is_bit_vector t then "bvupdate" else "update" in + let epp = align (string call ^//^ group (group (expY v) ^/^ group (expY e1) ^/^ group (expY e2)) ^/^ group (expY e3)) in if aexp_needed then parens (align epp) else epp @@ -670,9 +800,13 @@ let doc_exp_lem, doc_let_lem = (match annot with | Base((_,t),External(Some name),_,_,_,_) -> let argpp arg = - let (E_aux (_,(_,Base((_,{t=t}),_,_,_,_,_)))) = arg in - match t with - | Tapp("vector",_) -> parens (concat [string "reset_vector_start";space;expY arg]) + let (E_aux (_,(_,Base((_,t),_,_,_,_,_)))) = arg in + match t.t with + | Tapp("vector",_) -> + let call = + if is_bit_vector t then "reset_bitvector_start" + else "reset_vector_start" in + parens (concat [string call;space;expY arg]) | _ -> expY arg in let epp = let aux name = align (argpp e1 ^^ space ^^ string name ^//^ argpp e2) in @@ -740,6 +874,10 @@ let doc_exp_lem, doc_let_lem = | _ -> string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in + let (epp,aexp_needed) = + if contains_bitvector_type t && not (contains_t_pp_var t) + then (parens epp ^^ doc_tannot_lem regtypes false t, true) + else (epp, aexp_needed) in if aexp_needed then parens (align epp) else epp | _ -> let epp = diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml index 3772f549..adca6b12 100644 --- a/src/pretty_print_ocaml.ml +++ b/src/pretty_print_ocaml.ml @@ -338,10 +338,7 @@ let doc_exp_ocaml, doc_let_ocaml = | Typ_var (Kid_aux (Var "length",_)) -> parens ((string "set_start_to_length") ^//^ exp e) | _ -> - parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ))) - - -) + parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ)))) | E_tuple exps -> parens (separate_map comma exp exps) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> @@ -753,4 +750,3 @@ let pp_defs_ocaml f d top_line opens = print f (string "(*" ^^ (string top_line) ^^ string "*)" ^/^ (separate_map hardline (fun lib -> (string "open") ^^ space ^^ (string lib)) opens) ^/^ (doc_defs_ocaml d)) - diff --git a/src/type_internal.ml b/src/type_internal.ml index 2932cf33..3df352ae 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -560,15 +560,6 @@ let rec pow_i i n = | n -> mult_int_big_int i (pow_i i (n-1)) let two_pow = pow_i 2 -let is_bit_vector t = match t.t with - | Tapp("vector", [_;_;_; TA_typ t]) - | Tabbrev(_,{t=Tapp("vector",[_;_;_; TA_typ t])}) - | Tapp("reg", [TA_typ {t=Tapp("vector",[_;_;_; TA_typ t])}])-> - (match t.t with - | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) | Tapp("reg",[TA_typ {t=Tid "bit"}]) -> true - | _ -> false) - | _ -> false - (* predicate to determine if pushing a constant in for addition or multiplication could change the form *) let rec contains_const n = match n.nexp with @@ -929,8 +920,37 @@ let rec normalize_n_rec recur_ok n = let normalize_nexp = normalize_n_rec true +let rec normalize_t t = match t.t with + | Tfn (t1,t2,i,eff) -> {t = Tfn (normalize_t t1,normalize_t t2,i,eff)} + | Ttup ts -> {t = Ttup (List.map normalize_t ts)} + | Tapp (c,args) -> {t = Tapp (c, List.map normalize_t_arg args)} + | Tabbrev (_,t') -> t' + | _ -> t +and normalize_t_arg targ = match targ with + | TA_typ t -> TA_typ (normalize_t t) + | TA_nexp nexp -> TA_nexp (normalize_nexp nexp) + | _ -> targ + let int_to_nexp = mk_c_int +let rec is_bit_vector t = match t.t with + | Tapp("vector", [_;_;_; TA_typ t]) -> + (match t.t with + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) | Tapp("register",[TA_typ {t=Tid "bit"}]) -> true + | _ -> false) + | Tapp("register", [TA_typ t']) -> is_bit_vector t' + | Tabbrev(_,t') -> is_bit_vector t' + | _ -> false + +let rec has_const_vector_length t = match t.t with + | Tapp("vector", [_;TA_nexp m;_;_]) -> + (match (normalize_nexp m).nexp with + | Nconst i -> Some i + | _ -> None) + | Tapp("register", [TA_typ t']) -> has_const_vector_length t' + | Tabbrev(_,t') -> has_const_vector_length t' + | _ -> None + let v_count = ref 0 let t_count = ref 0 let tuvars = ref [] diff --git a/src/type_internal.mli b/src/type_internal.mli index ee2e3988..f4924a63 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -313,6 +313,7 @@ val get_abbrev : def_envs -> t -> (t * nexp_range list) val is_enum_typ : def_envs -> t -> int option val is_bit_vector : t -> bool +val has_const_vector_length : t -> big_int option val extract_bounds : def_envs -> string -> t -> bounds_env val merge_bounds : bounds_env -> bounds_env -> bounds_env @@ -324,6 +325,7 @@ val merge_option_maps : nexp_map option -> nexp_map option -> nexp_map option val expand_nexp : nexp -> nexp list val normalize_nexp : nexp -> nexp +val normalize_t : t -> t val get_index : nexp -> int (*expose nindex through this for debugging purposes*) val get_all_nvar : nexp -> string list (*Pull out all of the contained nvar and nuvars in nexp*) @@ -387,4 +389,3 @@ val tannot_merge : constraint_origin -> def_envs -> bool -> tannot -> tannot -> val initial_typ_env : tannot Envmap.t val initial_typ_env_list : (string * ((string * tannot) list)) list - |