diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_values.ml | 46 | ||||
| -rw-r--r-- | src/pretty_print.ml | 31 | ||||
| -rw-r--r-- | src/rewriter.ml | 3 |
3 files changed, 66 insertions, 14 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 4713f9a7..0072d5b6 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -3,7 +3,7 @@ open Big_int_Z (* only expected to be 0, 1, 2; 2 represents undef *) type vbit = Vone | Vzero | Vundef type number = Big_int_Z.big_int - +type _bool = vbit type value = | Vvector of vbit array * int * bool | VvectorR of value array * int * bool @@ -20,6 +20,10 @@ let is_one_big i = then Vone else Vzero + +let exit _ = failwith "called exit" + + let is_one i = if i = 1 then Vone else Vzero @@ -40,11 +44,19 @@ let get_start = function | Vvector(_,s,o) | Vregister(_,s,o,_) | VvectorR(_,s,o) -> s | _ -> assert false +let set_start i = function + | Vvector(a,start,dir) -> Vvector(a,i,dir) + | Vregister(bits,start,dir,regfields) -> Vregister(bits,i,dir,regfields) + | VvectorR(a,start,dir) -> VvectorR(a,i,dir) + | _ -> assert false + let length = function | Vvector(array,_,_) -> Array.length array | Vregister(array,_,_,_) -> Array.length !array | VvectorR(array,_,_) -> Array.length array | _ -> assert false + +let set_start_to_length v = set_start (length v) v let length_big v = big_int_of_int (length v) @@ -779,8 +791,8 @@ let rec arith_op_no0 op (l,r) = then None else Some (op l r) -let modulo = arith_op_no0 (mod) -let quot = arith_op_no0 (/) +let modulo = arith_op (mod) +let quot = arith_op (/) let rec arith_op_vec_no0 op sign size (l,r) = let ord = get_ord l in @@ -986,9 +998,35 @@ let gteq_range_vec_big = compare_op_range_vec_big ge_big_int true let eq (l,r) = if l == r then Vone else Vzero +let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) +let eq_vec (l,r) = eq_vec_vec(l,r) let eq_vec_range (l,r) = eq (to_num false l,r) let eq_range_vec (l,r) = eq (l, to_num false r) -let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) +let eq_range = eq +let eq_bit = bitwise_binop_bit (=) let neq (l,r) = bitwise_not_bit (eq (l,r)) let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec(l,r)) +let neq_bit (l,r) = bitwise_not_bit (eq_bit(l,r)) + +let mask (n,v) = match v with + | Vvector (bits,start,dir) -> + let current_size = Array.length bits in + let to_drop = (current_size - n) in + let bits' = Array.sub bits to_drop n in + Vvector (bits',(if dir then 0 else n-1), dir) + | VvectorR (bits,start,dir) -> + let current_size = Array.length bits in + let to_drop = (current_size - n) in + let bits' = Array.sub bits to_drop n in + VvectorR (bits',(if dir then 0 else n-1), dir) + | Vregister _ -> failwith "mask not implemented for Vregister" + | Vbit _ -> failwith "mask called for bit" + +let slice_raw (v, i, j) = match v with + | Vvector (bs, start, is_inc) -> + let bits = Array.sub bs i j in + let len = Array.length bits in + Vvector (bits, (if is_inc then 0 else len - 1), is_inc) + | _ -> failwith "slice_raw only implemented for VVector" +let _slice_raw = slice_raw diff --git a/src/pretty_print.ml b/src/pretty_print.ml index d526a6ed..83b0cabf 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1535,7 +1535,7 @@ let doc_id_ocaml (Id_aux(i,_)) = | Id("bit") -> string "vbit" | Id i -> string (if i.[0] = '\'' || is_number(i.[0]) then "_" ^ i - else String.uncapitalize i) + else "_" ^ (String.uncapitalize i)) | DeIid x -> (* add an extra space through empty to avoid a closing-comment * token in case of x ending with star. *) @@ -1544,7 +1544,7 @@ let doc_id_ocaml (Id_aux(i,_)) = let doc_id_ocaml_type (Id_aux(i,_)) = match i with | Id("bit") -> string "vbit" - | Id i -> string (String.uncapitalize i) + | Id i -> string ("_" ^ (String.uncapitalize i)) | DeIid x -> (* add an extra space through empty to avoid a closing-comment * token in case of x ending with star. *) @@ -1637,9 +1637,9 @@ let doc_pat_ocaml = | P_typ(typ,p) -> doc_op colon (pat p) (doc_typ_ocaml typ) | P_app(id,[]) -> (match annot with - | Base(_,Constructor n,_,_,_,_) -> + | Base(_,(Constructor n | Enum n),_,_,_,_) -> doc_id_ocaml_ctor n id - | _ -> empty) + | _ -> failwith "encountered unexpected P_app pattern") | P_vector pats -> let non_bit_print () = parens @@ -1798,7 +1798,19 @@ let doc_exp_ocaml, doc_let_ocaml = if read_registers then parens (string "read_register" ^^ space ^^ exp e) else exp e - | _ -> (parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ)))) + | _ -> + let (Typ_aux (t,_)) = typ in + (match t with + | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) -> + parens ((concat [string "set_start";space;string (string_of_int i)]) ^//^ + exp e) + | 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))) + + +) | E_tuple exps -> parens (separate_map comma exp exps) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> @@ -2132,7 +2144,8 @@ let doc_dec_ocaml (DEC_aux (reg,(l,annot))) = (match annot with | Base((_,t),_,_,_,_,_) -> (match t.t with - | Tapp("register", [TA_typ {t= Tapp("vector", [TA_nexp start; TA_nexp size; TA_ord order; TA_typ itemt])}]) -> + | Tapp("register", [TA_typ {t= Tapp("vector", [TA_nexp start; TA_nexp size; TA_ord order; TA_typ itemt])}]) + | Tapp("register", [TA_typ {t= Tabbrev(_,{t=Tapp("vector", [TA_nexp start; TA_nexp size; TA_ord order; TA_typ itemt])})}]) -> (match itemt.t,start.nexp,size.nexp with | Tid "bit", Nconst start, Nconst size -> let o = if order.order = Oinc then string "true" else string "false" in @@ -2154,10 +2167,10 @@ let doc_dec_ocaml (DEC_aux (reg,(l,annot))) = separate space [string "let"; doc_id_ocaml id; equals; - string idt; + doc_id_ocaml (Id_aux (Id idt, Unknown)); string "None"] - |_-> empty) - | _ -> empty) + |_-> failwith "type was not handled in register declaration") + | _ -> failwith "annot was not Base") | DEC_alias(id,alspec) -> empty (* doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec) *) | DEC_typ_alias(typ,id,alspec) -> empty (* diff --git a/src/rewriter.ml b/src/rewriter.ml index dc96b952..bd0670f4 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -1347,7 +1347,8 @@ let rewrite_defs_separate_numbs defs = rewrite_defs_base rewrite_defs = rewrite_defs_base} defs let rewrite_defs_ocaml defs = - let defs_vec_concat_removed = rewrite_defs_remove_vector_concat defs in + let defs_sorted = top_sort_defs defs in + let defs_vec_concat_removed = rewrite_defs_remove_vector_concat defs_sorted in let defs_lifted_assign = rewrite_defs_exp_lift_assign defs_vec_concat_removed in let defs_separate_nums = rewrite_defs_separate_numbs defs_lifted_assign in defs_separate_nums |