diff options
| -rw-r--r-- | src/gen_lib/sail_values.ml | 215 | ||||
| -rw-r--r-- | src/pretty_print.ml | 201 | ||||
| -rw-r--r-- | src/process_file.ml | 6 | ||||
| -rw-r--r-- | src/test/test1.sail | 2 | ||||
| -rw-r--r-- | src/type_internal.ml | 6 | ||||
| -rw-r--r-- | src/util.ml | 5 | ||||
| -rw-r--r-- | src/util.mli | 2 |
7 files changed, 321 insertions, 116 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index c8181572..42f0bfde 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -6,8 +6,8 @@ type number = Big_int_Z.big_int type value = | Vvector of vbit array * int * bool - | VvectorR of value ref array * int * bool - | Vregister of vbit array * int * bool * (string * (int * int)) list + | VvectorR of value array * int * bool + | Vregister of vbit array ref * int * bool * (string * (int * int)) list | Vbit of vbit (*Mostly for Vundef in place of undefined register place holders*) let to_bool = function @@ -16,26 +16,48 @@ let to_bool = function | Vundef -> assert false let get_barray = function - | Vvector(a,_,_) - | Vregister(a,_,_,_) -> a + | Vvector(a,_,_) -> a + | Vregister(a,_,_,_) -> !a | _ -> assert false let get_varray = function | VvectorR(a,_,_) -> a | _ -> assert false +let get_ord = function + | Vvector(_,_,o) | Vregister(_,_,o,_) | VvectorR(_,_,o) -> o + | _ -> assert false + +let get_start = function + | Vvector(_,s,o) | Vregister(_,s,o,_) | VvectorR(_,s,o) -> s + | _ -> assert false + +let length = function + | Vvector(array,_,_) -> big_int_of_int (Array.length array) + | Vregister(array,_,_,_) -> big_int_of_int (Array.length !array) + | VvectorR(array,_,_) -> big_int_of_int (Array.length array) + | _ -> assert false + +let read_register = function + | Vregister(a,start,inc,_) -> Vvector(!a,start,inc) + | v -> v + let vector_access v n = match v with | VvectorR(array,start,is_inc) -> if is_inc - then !(array.(n-start)) - else !(array.(start-n)) + then (array.(n-start)) + else (array.(start-n)) | _ -> assert false let bit_vector_access v n = match v with - | Vvector(array,start,is_inc) | Vregister(array,start,is_inc,_) -> + | Vvector(array,start,is_inc) -> if is_inc then array.(n-start) else array.(start-n) + | Vregister(array,start,is_inc,_) -> + if is_inc + then !array.(n-start) + else !array.(start-n) | _ -> assert false let vector_subrange v n m = @@ -51,28 +73,149 @@ let vector_subrange v n m = match v with | VvectorR(array,start,is_inc) -> let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in - VvectorR(builder array length offset (ref (VvectorR([||], 0, is_inc))),n,is_inc) + VvectorR(builder array length offset (VvectorR([||], 0, is_inc)),n,is_inc) | Vvector(array,start,is_inc) -> let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in Vvector(builder array length offset Vzero,n,is_inc) | Vregister(array,start,is_inc,fields) -> let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in - Vvector(builder array length offset Vzero,n,is_inc) + Vvector(builder !array length offset Vzero,n,is_inc) | _ -> v -let vector_append l r = +let get_register_field_vec reg field = + match reg with + | Vregister(_,_,_,fields) -> + (match List.assoc field fields with + | (i,j) -> + if i = j + then Vbit Vundef + else vector_subrange reg i j) + | _ -> Vbit Vundef + +let get_register_field_bit reg field = + match reg with + | Vregister(_,_,_,fields) -> + (match List.assoc field fields with + | (i,j) -> + if i = j + then bit_vector_access reg i + else Vundef) + | _ -> Vundef + +let set_register register value = match register,value with + | Vregister(a,_,_,_), Vregister(new_v,_,_,_) -> + a := !new_v + | Vregister(a,_,_,_), Vvector(new_v,_,_) -> + a := new_v + | _ -> () + +let set_vector_subrange_vec v n m new_v = + let walker array length offset new_values = + begin + for x = 0 to length-1 + do array.(x+offset) <- new_values.(x) + done; + end + in + match v with + | VvectorR(array,start,is_inc) -> + let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in + walker array length offset new_v + | _ -> () + +let set_vector_subrange_bit v n m new_v = + let walker array length offset new_values = + begin + for x = 0 to length-1 + do array.(x+offset) <- new_values.(x) + done; + end + in + match v with + | Vvector(array,start,is_inc) -> + let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in + walker array length offset new_v + | Vregister(array,start,is_inc,fields) -> + let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in + walker !array length offset new_v + | _ -> () + +let set_register_field_v reg field new_v = + match reg with + | Vregister(array,start,dir,fields) -> + (match List.assoc field fields with + | (i,j) -> + if i = j + then () + else set_vector_subrange_bit reg i j new_v) + | _ -> () + +let set_register_field_bit reg field new_v = + match reg with + | Vregister(array,start,dir,fields) -> + (match List.assoc field fields with + | (i,j) -> + if i = j + then !array.(if dir then i - start else start - i) <- new_v + else ()) + | _ -> () + +let set_two_reg r1 r2 vec = + let size = int_of_big_int (length r1) in + let dir = get_ord r1 in + let start = get_start vec in + let vsize = int_of_big_int (length vec) in + let r1_v = vector_subrange vec start ((if dir then size - start else start - size) - 1) in + let r2_v = vector_subrange vec (if dir then size - start else start - size) + (if dir then vsize - start else start - vsize) in + begin set_register r1 r1_v; set_register r2 r2_v end + + +let make_indexed_v entries default start size dir = + let default_value = match default with + | None -> Vbit Vundef + | Some v -> v in + let array = Array.make size default_value in + begin + List.iter (fun (i,v) -> array.(if dir then start - i else i - start) <- v) entries; + VvectorR(array, start, dir) + end + +let make_indexed_bitv entries default start size dir = + let default_value = match default with + | None -> Vundef + | Some v -> v in + let array = Array.make size default_value in + begin + List.iter (fun (i,v) -> array.(if dir then start - i else i - start) <- v) entries; + Vvector(array, start, dir) + end + +let vector_concat l r = match l,r with - | Vvector(arrayl,start,ord), Vvector(arrayr,_,_) - | Vvector(arrayl,start,ord), Vregister(arrayr,_,_,_) - | Vregister(arrayl,start,ord,_), Vvector(arrayr,_,_) + | Vvector(arrayl,start,ord), Vvector(arrayr,_,_) -> + Vvector(Array.append arrayl arrayr, start, ord) + | Vvector(arrayl,start,ord), Vregister(arrayr,_,_,_) -> + Vvector(Array.append arrayl !arrayr, start,ord) + | Vregister(arrayl,start,ord,_), Vvector(arrayr,_,_) -> + Vvector(Array.append !arrayl arrayr, start, ord) | Vregister(arrayl,start,ord,_), Vregister(arrayr,_,_,_) -> - Vvector(Array.append arrayl arrayr,start,ord) + Vvector(Array.append !arrayl !arrayr,start,ord) | VvectorR(arrayl,start,ord),VvectorR(arrayr,_,_) -> VvectorR(Array.append arrayl arrayr, start,ord) | _ -> Vbit Vundef let has_undef = function - | Vvector(array,_,_) | Vregister(array,_,_,_) -> + | Vvector(array,_,_) -> + let rec foreach i = + if i <= Array.length array + then + if array.(i) = Vundef then true + else foreach (i+1) + else false in + foreach 0 + | Vregister(array,_,_,_) -> + let array = !array in let rec foreach i = if i <= Array.length array then @@ -83,7 +226,8 @@ let has_undef = function | _ -> false let most_significant = function - | Vvector(array,_,_) | Vregister(array,_,_,_) -> array.(0) + | Vvector(array,_,_) -> array.(0) + | Vregister(array,_,_,_) -> !array.(0) | _ -> assert false let bitwise_not_bit = function @@ -92,11 +236,12 @@ let bitwise_not_bit = function | _ -> Vundef let bitwise_not = function - | Vvector(array,s,d) | Vregister(array,s,d,_) -> Vvector( Array.map bitwise_not_bit array,s,d) - | _ -> assert false + | Vvector(array,s,d)-> Vvector( Array.map bitwise_not_bit array,s,d) + | Vregister(array,s,d,_) -> Vvector( Array.map bitwise_not_bit !array,s,d) + | _ -> assert false let unsigned = function - | (Vvector(array,_,_) as v) | (Vregister(array,_,_,_) as v)-> + | (Vvector(array,_,_) as v) -> if has_undef v then assert false else @@ -107,7 +252,20 @@ let unsigned = function | _ -> () done; !acc - end + end + | (Vregister(array,_,_,_) as v)-> + let array = !array in + if has_undef v + then assert false + else + let acc = ref zero_big_int in + begin for i = (Array.length array) - 1 downto 0 do + match array.(i) with + | Vone -> acc := add_big_int !acc (power_int_positive_int 2 i) + | _ -> () + done; + !acc + end | _ -> assert false let signed v = @@ -184,10 +342,6 @@ let to_vec ord len n = let to_vec_inc (len,n) = to_vec true len n let to_vec_dec (len,n) = to_vec false len n -let length = function - | Vvector(array,_,_) | Vregister(array,_,_,_) -> big_int_of_int (Array.length array) - | VvectorR(array,_,_) -> big_int_of_int (Array.length array) - | _ -> assert false let arith_op op (l,r) = op l r let add = arith_op add_big_int @@ -198,10 +352,6 @@ let modulo = arith_op mod_big_int let quot = arith_op div_big_int let power = arith_op power_big -let get_ord = function - | Vvector(_,_,o) | Vregister(_,_,o,_) | VvectorR(_,_,o) -> o - | _ -> assert false - let arith_op_vec op sign size (l,r) = let ord = get_ord l in let (l',r') = to_num sign l, to_num sign r in @@ -314,22 +464,23 @@ let minus_overflow_vec_bit_signed = arith_op_overflow_vec_bit sub_big_int true u let shift_op_vec op (l,r) = match l with - | Vvector(array,start,ord) | Vregister(array,start,ord,_) -> + | Vvector(_,start,ord) | Vregister(_,start,ord,_) -> + let array = match l with | Vvector(array,_,_) -> array | Vregister(array,_,_,_) -> !array | _ -> assert false in let len = Array.length array in let n = int_of_big_int r in (match op with | "<<" -> let right_vec = Vvector(Array.make n Vzero,0,true) in let left_vec = vector_subrange l n (if ord then len + start else start - len) in - vector_append left_vec right_vec + vector_concat left_vec right_vec | ">>" -> let right_vec = vector_subrange l start n in let left_vec = Vvector(Array.make n Vzero,0,true) in - vector_append left_vec right_vec + vector_concat left_vec right_vec | "<<<" -> let left_vec = vector_subrange l n (if ord then len + start else start - len) in let right_vec = vector_subrange l start n in - vector_append left_vec right_vec + vector_concat left_vec right_vec | _ -> assert false) | _ -> assert false diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 9b5173c3..322091f0 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1204,7 +1204,7 @@ let star_sp = star ^^ space let doc_id_ocaml (Id_aux(i,_)) = match i with | Id("bit") -> string "vbit" - | Id i -> string (if i.[0] = '\'' then "_" ^ i else i) + | Id i -> string (if i.[0] = '\'' then "_" ^ 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. *) @@ -1252,7 +1252,7 @@ let doc_typ_ocaml, doc_atomic_typ_ocaml = | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) -> (string "number") | Typ_app(id,args) -> - (separate_map space doc_typ_arg_ocaml args) ^^ (doc_id_ocaml_type id) + (separate_map space doc_typ_arg_ocaml args) ^^ space ^^ (doc_id_ocaml_type id) | _ -> atomic_typ ty and atomic_typ ((Typ_aux (t, _)) as ty) = match t with | Typ_id id -> doc_id_ocaml_type id @@ -1269,16 +1269,16 @@ let doc_typ_ocaml, doc_atomic_typ_ocaml = | Typ_arg_effect e -> empty in typ, atomic_typ -let doc_lit_ocaml (L_aux(l,_)) = +let doc_lit_ocaml in_pat (L_aux(l,_)) = utf8string (match l with | L_unit -> "()" | L_zero -> "Vzero" | L_one -> "Vone" | L_true -> "Vone" | L_false -> "Vzero" - | L_num i -> string_of_int i - | L_hex n -> "(num_to_vec" ^ ("0x" ^ n) ^ ")" (*shouldn't happen*) - | L_bin n -> "(num_to_vec" ^ ("0b" ^ n) ^ ")" (*shouldn't happen*) + | L_num i -> if in_pat then string_of_int i else "(big_int_of_int " ^ string_of_int i ^ ")" + | L_hex n -> "(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*) + | L_bin n -> "(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*) | L_undef -> "Vundef" | L_string s -> "\"" ^ s ^ "\"") @@ -1291,15 +1291,13 @@ let doc_typscm_ocaml (TypSchm_aux(TypSchm_ts(tq,t),_)) = (*Note: vector concatenation, literal vectors, indexed vectors, and record should be removed prior to pp. The latter two have never yet been seen *) -let doc_pat_ocaml, doc_atomic_pat_ocaml = +let doc_pat_ocaml = let rec pat pa = app_pat pa - and app_pat ((P_aux(p,l)) as pa) = match p with - | P_app(id, ((_ :: _) as pats)) -> doc_unop (doc_id_ocaml_ctor id) (parens (separate_map comma_sp atomic_pat pats)) - | _ -> atomic_pat pa - and atomic_pat ((P_aux(p,(l,annot))) as pa) = match p with - | P_lit lit -> doc_lit lit + and app_pat ((P_aux(p,(l,annot))) as pa) = match p with + | P_app(id, ((_ :: _) as pats)) -> doc_unop (doc_id_ocaml_ctor id) (parens (separate_map comma_sp pat pats)) + | P_lit lit -> doc_lit_ocaml true lit | P_wild -> underscore - | P_id id -> doc_id id + | P_id id -> doc_id_ocaml id | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id_ocaml id]) | P_typ(typ,p) -> doc_op colon (pat p) (doc_typ_ocaml typ) | P_app(id,[]) -> doc_id_ocaml_ctor id @@ -1311,12 +1309,14 @@ let doc_pat_ocaml, doc_atomic_pat_ocaml = then parens (separate space [string "Vvector"; squarebars (separate_map semi pat pats); underscore ; underscore]) else non_bit_print() | _ -> non_bit_print ()) - | P_tup pats -> parens (separate_map comma_sp atomic_pat pats) + | P_tup pats -> parens (separate_map comma_sp pat pats) | P_list pats -> brackets (separate_map semi pat pats) (*Never seen but easy in ocaml*) - in pat, atomic_pat + in pat let doc_exp_ocaml, doc_let_ocaml = - let rec exp (E_aux (e, (_,annot))) = match e with + let rec top_exp read_registers (E_aux (e, (_,annot))) = + let exp = top_exp read_registers in + match e with | E_assign((LEXP_aux(le_act,tannot) as le),e) -> (match annot with | Base(_,(Emp_local | Emp_set),_,_,_,_) -> @@ -1325,16 +1325,16 @@ let doc_exp_ocaml, doc_let_ocaml = (*Setting local variable fully *) doc_op coloneq (doc_lexp_ocaml le) (exp e) | LEXP_vector _ -> - doc_op (string "<-") (doc_lexp_ocaml le) (exp e) + doc_op (string "<-") (doc_lexp_array_ocaml le) (exp e) | LEXP_vector_range _ -> - group ((string "set_vector_range") ^^ space ^^ (doc_lexp_ocaml le) ^^ space ^^ (exp e))) + parens ((string "set_vector_range") ^^ space ^^ (doc_lexp_ocaml le) ^^ space ^^ (exp e))) | _ -> (match le_act with | LEXP_vector _ | LEXP_vector_range _ | LEXP_cast _ | LEXP_field _ | LEXP_id _ -> (doc_lexp_rwrite le e) | LEXP_memory _ -> (doc_lexp_fcall le e))) | E_vector_append(l,r) -> - group (parens (string "vector_append ") ^^ (exp l) ^^ space ^^ (exp r)) + parens (string "vector_concat ") ^^ (exp l) ^^ space ^^ (exp r) | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r) | E_if(c,t,E_aux(E_block [], _)) -> string "if" ^^ space ^^ string "to_bool" ^^ parens (exp c) ^/^ @@ -1399,7 +1399,12 @@ let doc_exp_ocaml, doc_let_ocaml = (match fannot with | Base((_,{t= Tapp("register",_)}),_,_,_,_,_) | Base((_,{t= Tabbrev(_,{t=Tapp("register",_)})}),_,_,_,_,_)-> - parens ((string "get_register_field") ^^ space ^^ (exp fexp) ^^ space ^^ string_lit (doc_id id)) + let field_f = match annot with + | Base((_,{t = Tid "bit"}),_,_,_,_,_) | + Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) -> + string "get_register_field_bit" + | _ -> string "get_register_field_vec" in + parens (field_f ^^ space ^^ (exp fexp) ^^ space ^^ string_lit (doc_id id)) | _ -> exp fexp ^^ dot ^^ doc_id id) | E_block [] -> string "()" | E_block exps | E_nondet exps -> @@ -1409,21 +1414,34 @@ let doc_exp_ocaml, doc_let_ocaml = (match annot with | Base((_, ({t = Tapp("reg",_)} | {t=Tabbrev(_,{t=Tapp("reg",_)})})),_,_,_,_,_) -> string "!" ^^ doc_id_ocaml id - | Base((_,({t=Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})), External _,_,_,_,_) -> - string "!" ^^ doc_id_ocaml id - | Base(_,Alias alias_info,_,_,_,_) -> + | Base((_, ({t = Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})),_,_,_,_,_) -> + if read_registers + then string "(read_register " ^^ doc_id_ocaml id ^^ string ")" + else doc_id_ocaml id + | Base(_,(Constructor|Enum _),_,_,_,_) -> doc_id_ocaml_ctor id + | Base((_,t),Alias alias_info,_,_,_,_) -> (match alias_info with | Alias_field(reg,field) -> - parens (string "get_register_field" ^^ space ^^ string reg ^^ string_lit (string field)) + let field_f = match t.t with + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> string "get_register_field_bit" + | _ -> string "get_register_field_vec" in + parens (separate space [field_f; string reg; string_lit (string field)]) | Alias_extract(reg,start,stop) -> if start = stop - then parens (string "bit_vector_access" ^^ space ^^ string reg ^^ space ^^ doc_int start) - else parens (string "vector_subrange" ^^ space ^^ string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop) + then parens (separate space [string "bit_vector_access";string reg;doc_int start]) + else parens + (separate space [string "vector_subrange"; string reg; doc_int start; doc_int stop]) | Alias_pair(reg1,reg2) -> - parens (string "vector_append" ^^ space ^^ string reg1 ^^ space ^^ string reg2)) + parens (separate space [string "vector_concat"; string reg1; string reg2])) | _ -> doc_id_ocaml id) - | E_lit lit -> doc_lit lit - | E_cast(typ,e) -> (parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ))) + | E_lit lit -> doc_lit_ocaml false lit + | E_cast(typ,e) -> + (match annot with + | Base(_,External _,_,_,_,_) -> + 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)))) | E_tuple exps -> parens (separate_map comma exp exps) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> @@ -1444,7 +1462,9 @@ let doc_exp_ocaml, doc_let_ocaml = | Nconst i -> string_of_big_int i | N2n(_,Some i) -> string_of_big_int i | _ -> if dir then "0" else string_of_int (List.length exps) in - group (call ^^ space ^^ squarebars (separate_map semi exp exps) ^^ string start ^^ string dir_out)) + parens (separate space [call; parens (separate comma_sp [squarebars (separate_map semi exp exps); + string start; + string dir_out])])) | E_vector_indexed (iexps, (Def_val_aux (default,_))) -> (match annot with | Base((_,t),_,_,_,_,_) -> @@ -1456,17 +1476,24 @@ let doc_exp_ocaml, doc_let_ocaml = | Oinc -> true,"true" | _ -> false, "false" in let start = match start.nexp with - | Nconst i -> string_of_big_int i - | N2n(_,Some i) -> string_of_big_int i + | Nconst i | N2n(_,Some i)-> string_of_big_int i + | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i)) | _ -> if dir then "0" else string_of_int (List.length iexps) in let size = match len.nexp with - | Nconst i | N2n(_,Some i)-> string_of_big_int i in + | Nconst i | N2n(_,Some i)-> string_of_big_int i + | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i)) + in let default_string = (match default with | Def_val_empty -> string "None" | Def_val_dec e -> parens (string "Some " ^^ (exp e))) in let iexp (i,e) = parens (separate_map comma_sp (fun x -> x) [(doc_int i); (exp e)]) in - group (call ^^ (brackets (separate_map semi iexp iexps)) ^^ space ^^ default_string ^^ string start ^^ string size ^^ string dir_out)) + parens (separate space [call; + (brackets (separate_map semi iexp iexps)); + default_string; + string start; + string size; + string dir_out])) | E_vector_update(v,e1,e2) -> (*Has never happened to date*) brackets (doc_op (string "with") (exp v) (doc_op equals (exp e1) (exp e2))) @@ -1476,9 +1503,9 @@ let doc_exp_ocaml, doc_let_ocaml = doc_op (string "with") (exp v) (doc_op equals (exp e1 ^^ colon ^^ exp e2) (exp e3))) | E_list exps -> - brackets (separate_map comma exp exps) + brackets (separate_map semi exp exps) | E_case(e,pexps) -> - let opening = separate space [string "("; string "match"; exp e; string "with"] in + let opening = separate space [string "("; string "match"; top_exp true e; string "with"] in let cases = separate_map (break 1) doc_case pexps in surround 2 1 opening cases rparen | E_exit e -> @@ -1507,34 +1534,50 @@ let doc_exp_ocaml, doc_let_ocaml = and let_exp (LB_aux(lb,_)) = match lb with | LB_val_explicit(ts,pat,e) -> prefix 2 1 - (separate space [string "let"; doc_atomic_pat_ocaml pat; equals]) - (exp e) + (separate space [string "let"; doc_pat_ocaml pat; equals]) + (top_exp false e) | LB_val_implicit(pat,e) -> prefix 2 1 - (separate space [string "let"; doc_atomic_pat_ocaml pat; equals]) - (exp e) + (separate space [string "let"; doc_pat_ocaml pat; equals]) + (top_exp false e) - and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id_ocaml id) (exp e) + and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id_ocaml id) (top_exp false e) and doc_case (Pat_aux(Pat_exp(pat,e),_)) = - doc_op arrow (separate space [pipe; doc_atomic_pat_ocaml pat]) (group (exp e)) + doc_op arrow (separate space [pipe; doc_pat_ocaml pat]) (group (top_exp false e)) - and doc_lexp_ocaml ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with - | LEXP_vector(v,e) -> parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml v) ^^ dot ^^ parens (exp e) - | LEXP_vector_range(v,e1,e2) -> + and doc_lexp_ocaml ((LEXP_aux(lexp,(l,annot))) as le) = + let exp = top_exp false in + match lexp with + | LEXP_vector(v,e) -> parens ((string "vector_access") ^^ space ^^ doc_lexp_ocaml v) ^^ dot ^^ parens (exp e) + | LEXP_vector_range(v,e1,e2) -> parens ((string "vector_subrange") ^^ space ^^ doc_lexp_ocaml v ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) - | LEXP_field(v,id) -> doc_lexp_ocaml v ^^ dot ^^ doc_id_ocaml id - | LEXP_id id -> doc_id_ocaml id - | LEXP_cast(typ,id) -> (doc_id_ocaml id) + | LEXP_field(v,id) -> doc_lexp_ocaml v ^^ dot ^^ doc_id_ocaml id + | LEXP_id id -> doc_id_ocaml id + | LEXP_cast(typ,id) -> (doc_id_ocaml id) + + and doc_lexp_array_ocaml ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with + | LEXP_vector(v,e) -> parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml v) ^^ dot ^^ parens (top_exp false e) + | _ -> empty and doc_lexp_rwrite ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = + let exp = top_exp false in + let is_bit = match e_new_v with + | E_aux(_,(_,Base((_,t),_,_,_,_,_))) -> + (match t.t with + | Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))]) | + Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) -> + true + | _ -> false) + | _ -> false in match lexp with | LEXP_vector(v,e) -> doc_op (string "<-") - (group (parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml v)) ^^ dot ^^ parens (exp e)) + (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ doc_lexp_ocaml v)) ^^ + dot ^^ parens (exp e)) (exp e_new_v) | LEXP_vector_range(v,e1,e2) -> - parens ((string "set_vector_subrange") ^^ space ^^ + parens ((string (if is_bit then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^ doc_lexp_ocaml v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v) | LEXP_field(v,id) -> parens ((string "set_register_field") ^^ space ^^ @@ -1544,27 +1587,28 @@ let doc_exp_ocaml, doc_let_ocaml = | Base(_,Alias alias_info,_,_,_,_) -> (match alias_info with | Alias_field(reg,field) -> - parens ((string "set_register_field") ^^ space ^^ + parens ((if is_bit then string "set_register_field_bit" else string "set_register_field_v") ^^ space ^^ string reg ^^ space ^^string_lit (string field) ^^ space ^^ exp e_new_v) | Alias_extract(reg,start,stop) -> if start = stop then doc_op (string "<-") - (group (parens ((string "get_varray") ^^ space ^^ string reg)) ^^ dot ^^ parens (doc_int start)) + (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ string reg)) ^^ + dot ^^ parens (doc_int start)) (exp e_new_v) else - parens ((string "set_vector_subrange") ^^ space ^^ + parens ((string (if is_bit then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^ string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop ^^ space ^^ exp e_new_v) | Alias_pair(reg1,reg2) -> parens ((string "set_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v)) | _ -> - doc_op (string ":=") (doc_id_ocaml id) (exp e_new_v)) + parens (separate space [string "set_register"; doc_id_ocaml id; exp e_new_v])) and doc_lexp_fcall ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = match lexp with - | LEXP_memory(id,args) -> doc_id_ocaml id ^^ parens (separate_map comma exp (args@[e_new_v])) + | LEXP_memory(id,args) -> doc_id_ocaml id ^^ parens (separate_map comma (top_exp false) (args@[e_new_v])) (* expose doc_exp and doc_let *) - in exp, let_exp + in top_exp false, let_exp (*TODO Upcase and downcase type and constructors as needed*) let doc_type_union_ocaml (Tu_aux(typ_u,_)) = match typ_u with @@ -1600,24 +1644,24 @@ let doc_typdef_ocaml (TD_aux(td,_)) = match td with match n1,n2 with | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> let dir = i1 < i2 in - let size = if dir then i2-i1 -1 else i1-i2 -1 in + let size = if dir then i2-i1 else i1-i2 in doc_op equals ((string "let") ^^ space ^^ doc_id_ocaml id ^^ space ^^ (string "init_val")) - (separate space [string "ref"; - string "Vregister"; + (separate space [string "Vregister"; (parens (separate comma_sp [parens (separate space [string "match init_val with"; pipe; string "None"; arrow; - string "Array.make"; + string "ref"; + string "(Array.make"; doc_int size; - string "Vzero"; + string "Vzero)"; pipe; string "Some init_val"; arrow; - string "init_val";]); + string "ref init_val";]); doc_nexp n1; string (if dir then "true" else "false"); brackets doc_rids]))]) @@ -1644,12 +1688,13 @@ let doc_fundef_ocaml (FD_aux(FD_function(r, typa, efa, fcls),_)) = | _ -> let id = get_id fcls in let sep = hardline ^^ pipe ^^ space in - let clauses = separate_map sep doc_funcl fcls in + let clauses = separate_map sep doc_funcl_ocaml fcls in separate space [string "let"; doc_rec_ocaml r; doc_id_ocaml id; equals; (string "function"); + (hardline^^pipe); clauses] let doc_dec_ocaml (DEC_aux (reg,(l,annot))) = @@ -1665,18 +1710,18 @@ let doc_dec_ocaml (DEC_aux (reg,(l,annot))) = separate space [string "let"; doc_id_ocaml id; equals; - string "ref"; - parens (separate space - [string "Vregister"; - parens (separate comma [doc_int (int_of_big_int start); - o; - parens (separate space - [string "Array.make"; - doc_int (int_of_big_int size); - string "Vzero"; - string "[]"])])])] + string "Vregister"; + parens (separate comma [separate space [string "ref"; + parens (separate space + [string "Array.make"; + doc_int (int_of_big_int size); + string "Vzero";])]; + doc_int (int_of_big_int start); + o; + brackets empty])] | _ -> empty) - | Tapp("register", [TA_typ {t=Tid idt}]) -> + | Tapp("register", [TA_typ {t=Tid idt}]) | + Tabbrev( {t= Tid idt}, _) -> separate space [string "let"; doc_id_ocaml id; equals; @@ -1684,10 +1729,10 @@ let doc_dec_ocaml (DEC_aux (reg,(l,annot))) = string "None"] |_-> empty) | _ -> empty) - | DEC_alias(id,alspec) -> - doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec) - | DEC_typ_alias(typ,id,alspec) -> - doc_op equals (string "register alias" ^^ space ^^ doc_atomic_typ typ) (doc_alias alspec) + | 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 (* + doc_op equals (string "register alias" ^^ space ^^ doc_atomic_typ typ) (doc_alias alspec) *) let doc_def_ocaml def = group (match def with | DEF_default df -> empty diff --git a/src/process_file.ml b/src/process_file.ml index 5b6c8ee5..443ea9b0 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -174,7 +174,7 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo end | Lem_out None -> let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ "embed.lem") in - begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Sail_values"]; + begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Sail_values";]; close_output_with_check ext_o end | Lem_out (Some lib) -> @@ -183,12 +183,12 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo close_output_with_check ext_o | Ocaml_out None -> let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in - begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Sail_values"]; + begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"]; close_output_with_check ext_o end | Ocaml_out (Some lib) -> let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in - Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Sail_values"; lib]; + Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z"; "Sail_values"; lib]; close_output_with_check ext_o diff --git a/src/test/test1.sail b/src/test/test1.sail index 8143bf5d..0c08324c 100644 --- a/src/test/test1.sail +++ b/src/test/test1.sail @@ -12,7 +12,7 @@ typedef creg = register bits [5:10] { 5 : h ; 6..7 : j} let (bool) e = true val forall Nat 'a, Nat 'b. bit['a:'b] sliced let (bit) v = bitzero -let ( bit [ 32 ] ) v1 = 0b101 +let ( bit [ 3 ] ) v1 = 0b101 let ( bit [32] ) v2 = 0xABCDEF01 diff --git a/src/type_internal.ml b/src/type_internal.ml index 9d840639..af6626b8 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -2879,7 +2879,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e (t2,[GtEq(co,Require,b1,n_zero);LtEq(co,Require,r1,mk_c(big_int_of_int num_enums))],pure_e, E_aux(E_case(e, List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_lit(L_aux((L_num i),l)), (l,simple_annot t1)), - E_aux(E_id(Id_aux(Id a,l)), (l, simple_annot t2))), + E_aux(E_id(Id_aux(Id a,l)), + (l, tag_annot t2 (Enum num_enums)))), (l,simple_annot t2))) enums), (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e))))) | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2))) @@ -2891,7 +2892,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e LtEq(co,Require,b1,mk_c(big_int_of_int num_enums))],pure_e, E_aux(E_case(e, List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_lit(L_aux((L_num i),l)),(l, simple_annot t1)), - E_aux(E_id(Id_aux(Id a,l)),(l, simple_annot t2))), + E_aux(E_id(Id_aux(Id a,l)), + (l, tag_annot t2 (Enum num_enums)))), (l,simple_annot t2))) enums), (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e))))) | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2))) diff --git a/src/util.ml b/src/util.ml index 0ae3fcf7..a2bd7cc0 100644 --- a/src/util.ml +++ b/src/util.ml @@ -80,6 +80,11 @@ let remove_dups compare eq l = in aux [] l' +let rec power i tothe = + if tothe <= 0 + then 1 + else i * power i (tothe - 1) + let rec assoc_maybe eq l k = match l with | [] -> None diff --git a/src/util.mli b/src/util.mli index bc2a1261..45e20381 100644 --- a/src/util.mli +++ b/src/util.mli @@ -61,6 +61,8 @@ val remove_dups : ('a -> 'a -> int) -> ('a -> 'a -> bool) -> 'a list -> 'a list val assoc_maybe : ('a -> 'a -> bool) -> ('a * 'b) list -> 'a -> 'b option +val power : int -> int -> int + (** {2 Option Functions} *) (** [option_map f None] returns [None], whereas |