diff options
| -rw-r--r-- | src/gen_lib/sail_values.ml | 9 | ||||
| -rw-r--r-- | src/pretty_print.ml | 37 | ||||
| -rw-r--r-- | src/rewriter.ml | 70 | ||||
| -rw-r--r-- | src/type_check.ml | 37 | ||||
| -rw-r--r-- | src/type_internal.ml | 12 |
5 files changed, 124 insertions, 41 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index c789ff52..8a1a27c6 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -15,6 +15,11 @@ let to_bool = function | Vone -> true | Vundef -> assert false +let is_one i = + if eq_big_int i unit_big_int + then Vone + else Vzero + let get_barray = function | Vvector(a,_,_) -> a | Vregister(a,_,_,_) -> !a @@ -117,8 +122,8 @@ let set_vector_subrange_vec v n m new_v = done; end in - match v with - | VvectorR(array,start,is_inc) -> + match v, new_v with + | VvectorR(array,start,is_inc),VvectorR(new_v,_,_) -> 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 | _ -> () diff --git a/src/pretty_print.ml b/src/pretty_print.ml index db49989f..a4042588 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1447,14 +1447,16 @@ let doc_exp_ocaml, doc_let_ocaml = 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)]) + parens (separate space [field_f; string (String.uncapitalize reg); string_lit (string field)]) | Alias_extract(reg,start,stop) -> if start = stop - then parens (separate space [string "bit_vector_access";string reg;doc_int start]) + then parens (separate space [string "bit_vector_access";string (String.uncapitalize reg);doc_int start]) else parens - (separate space [string "vector_subrange"; string reg; doc_int start; doc_int stop]) + (separate space [string "vector_subrange"; string (String.uncapitalize reg); doc_int start; doc_int stop]) | Alias_pair(reg1,reg2) -> - parens (separate space [string "vector_concat"; string reg1; string reg2])) + parens (separate space [string "vector_concat"; + string (String.uncapitalize reg1); + string (String.uncapitalize reg2)])) | _ -> doc_id_ocaml id) | E_lit lit -> doc_lit_ocaml false lit | E_cast(typ,e) -> @@ -1492,7 +1494,8 @@ let doc_exp_ocaml, doc_let_ocaml = | Base((_,t),_,_,_,_,_) -> match t.t with | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _]) - | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}) -> + | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}) + | Tapp("reg", [TA_typ {t =Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}]) -> let call = if is_bit_vector t then (string "make_indexed_bitv") else (string "make_indexed_v") in let dir,dir_out = match order.order with | Oinc -> true,"true" @@ -1571,7 +1574,7 @@ let doc_exp_ocaml, doc_let_ocaml = and doc_lexp_ocaml top_call ((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 false v)) ^^ dot ^^ parens (exp e) + | LEXP_vector(v,e) -> doc_lexp_array_ocaml le | LEXP_vector_range(v,e1,e2) -> parens ((string "vector_subrange") ^^ space ^^ (doc_lexp_ocaml false v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) | LEXP_field(v,id) -> (doc_lexp_ocaml false v) ^^ dot ^^ doc_id_ocaml id @@ -1601,9 +1604,12 @@ let doc_exp_ocaml, doc_let_ocaml = | 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"})})])}) -> + Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) | + Tapp("reg", [TA_typ {t= Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))])}]) + -> (false,true) - | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> (true,false) + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) | Tapp("reg",[TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})]) + -> (true,false) | _ -> (false,false)) | _ -> (false,false) in match lexp with @@ -1613,7 +1619,7 @@ let doc_exp_ocaml, doc_let_ocaml = dot ^^ parens (exp e)) (exp e_new_v) | LEXP_vector_range(v,e1,e2) -> - parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^ + parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^ doc_lexp_ocaml false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v) | LEXP_field(v,id) -> parens ((string (if is_bit then "set_register_field_bit" else "set_register_field_v")) ^^ space ^^ @@ -1624,7 +1630,7 @@ let doc_exp_ocaml, doc_let_ocaml = (match alias_info with | Alias_field(reg,field) -> 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) + string (String.uncapitalize reg) ^^ space ^^string_lit (string field) ^^ space ^^ exp e_new_v) | Alias_extract(reg,start,stop) -> if start = stop then @@ -1633,7 +1639,7 @@ let doc_exp_ocaml, doc_let_ocaml = dot ^^ parens (doc_int start)) (exp e_new_v) else - parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^ + parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ 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)) @@ -2185,9 +2191,12 @@ let doc_exp_lem, doc_let_lem = | 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"})})])}) -> - (false,true) - | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> (true,false) + Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) | + Tapp("reg",[TA_typ {t = Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))])}]) + -> + (false,true) + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) | Tapp("reg",[TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})]) + -> (true,false) | _ -> (false,false)) | _ -> (false,false) in match lexp with diff --git a/src/rewriter.ml b/src/rewriter.ml index 30b6b3fe..bc7cba0d 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -865,6 +865,46 @@ let rewrite_exp_lift_assign_intro rewriters nmap ((E_aux (exp,(l,annot))) as ful let exps' = walker exps in [(E_aux (E_internal_let(le', e', E_aux(E_block exps', (l, simple_annot {t=Tid "unit"}))), (l, simple_annot t)))] + | ((E_aux(E_if(c,t,e),(l,annot))) as exp)::exps -> + let vars_t = introduced_variables t in + let vars_e = introduced_variables e in + let new_vars = Envmap.intersect vars_t vars_e in + if Envmap.is_empty new_vars + then (rewrite_base exp)::walker exps + else + let new_nmap = match nmap with + | None -> Some(Nexpmap.empty,new_vars) + | Some(nm,s) -> Some(nm, Envmap.union new_vars s) in + let c' = rewrite_base c in + let t' = rewriters.rewrite_exp rewriters new_nmap t in + let e' = rewriters.rewrite_exp rewriters new_nmap e in + Envmap.fold + (fun res i (t,e) -> + let bitlit = E_aux (E_lit (L_aux(L_zero, Parse_ast.Unknown)), + (Parse_ast.Unknown, simple_annot bit_t)) in + let rangelit = E_aux (E_lit (L_aux (L_num 0, Parse_ast.Unknown)), + (Parse_ast.Unknown, simple_annot nat_t)) in + let set_exp = + match t.t with + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> bitlit + | Tapp("range", _) | Tapp("atom", _) -> rangelit + | Tapp("vector", [_;_;_;TA_typ ( {t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})]) + | Tapp(("reg"|"register"),[TA_typ ({t = 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"})})])}) -> + E_aux (E_vector_indexed([], Def_val_aux(Def_val_dec bitlit, + (Parse_ast.Unknown,simple_annot bit_t))), + (Parse_ast.Unknown, simple_annot t)) + | _ -> e in + [E_aux (E_internal_let (LEXP_aux (LEXP_id (Id_aux (Id i, Parse_ast.Unknown)), + (Parse_ast.Unknown, (tag_annot t Emp_intro))), + set_exp, + E_aux (E_block res, (Parse_ast.Unknown, (simple_annot unit_t)))), + (Parse_ast.Unknown, simple_annot unit_t))]) + (E_aux(E_if(c',t',e'), (Parse_ast.Unknown, annot))::(walker exps)) new_vars | e::exps -> (rewrite_rec e)::(walker exps) in rewrap (E_block (walker exps)) @@ -872,16 +912,38 @@ let rewrite_exp_lift_assign_intro rewriters nmap ((E_aux (exp,(l,annot))) as ful (match annot with | Base((_,t),Emp_intro,_,_,_,_) -> let le' = rewriters.rewrite_lexp rewriters nmap le in - let e' = rewrite_base e in - rewrap (E_internal_let(le', e', E_aux(E_block [], (l, simple_annot {t=Tid "unit"})))) - | _ -> rewrite_base full_exp) + (match le' with + | LEXP_aux(_, (_,Base(_,Emp_intro,_,_,_,_))) -> + let e' = rewrite_base e in + rewrap (E_internal_let(le', e', E_aux(E_block [], (l, simple_annot unit_t)))) + | _ -> E_aux((E_assign(le', rewrite_base e)),(l, tag_annot unit_t Emp_set))) + | _ -> rewrite_base full_exp) | _ -> rewrite_base full_exp +let rewrite_lexp_lift_assign_intro rewriters map ((LEXP_aux(lexp,(l,annot))) as le) = + let rewrap le = LEXP_aux(le,(l,annot)) in + let rewrite_base = rewrite_lexp rewriters map in + match lexp with + | LEXP_id (Id_aux (Id i, _)) | LEXP_cast (_,(Id_aux (Id i,_))) -> + (match annot with + | Base((p,t),Emp_intro,cs,e1,e2,bs) -> + (match map with + | Some(_,s) -> + (match Envmap.apply s i with + | None -> rewrap lexp + | Some _ -> + let ls = BE_aux(BE_lset,l) in + LEXP_aux(lexp,(l,(Base((p,t),Emp_set,cs,add_effect ls e1, add_effect ls e2,bs))))) + | _ -> rewrap lexp) + | _ -> rewrap lexp) + | _ -> rewrite_base le + + let rewrite_defs_exp_lift_assign defs = rewrite_defs_base {rewrite_exp = rewrite_exp_lift_assign_intro; rewrite_pat = rewrite_pat; rewrite_let = rewrite_let; - rewrite_lexp = rewrite_lexp; + rewrite_lexp = rewrite_lexp_lift_assign_intro; rewrite_fun = rewrite_fun; rewrite_def = rewrite_def; rewrite_defs = rewrite_defs_base} defs diff --git a/src/type_check.ml b/src/type_check.ml index 4fb2cfc1..5bff7d3d 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -593,16 +593,18 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | L_undef -> let ef = {effect=Eset[BE_aux(BE_undef,l)]} in (match expect_t.t with - | Tapp ("vector",[TA_nexp base;TA_nexp {nexp = rise};TA_ord o;(TA_typ {t=Tid "bit"})]) - | Tapp ("register",[TA_typ {t=Tapp ("vector",[TA_nexp base;TA_nexp { nexp = rise}; - TA_ord o;(TA_typ {t=Tid "bit"})])}])-> + | Tapp ("vector",[TA_nexp base;TA_nexp rise;TA_ord o;(TA_typ {t=Tid "bit"})]) + | Toptions({t = Tapp ("vector",[TA_nexp base;TA_nexp rise;TA_ord o;(TA_typ {t=Tid "bit"})])}, None) -> let f = match o.order with | Oinc -> "to_vec_inc_undef" | Odec -> "to_vec_dec_undef" | _ -> (match d_env.default_o.order with | Oinc -> "to_vec_inc_undef" | Odec -> "to_vec_dec_undef" | _ -> "to_vec_inc_undef") in - let tannot = (l,Base(([],expect_t),External (Some f),[],ef,ef,b_env)) in + let _ = set_imp_param rise in + let internal_tannot = (l,(cons_bs_annot {t = Tapp("implicit",[TA_nexp rise])} [] b_env)) in + let tannot = (l,Base(([],{t = Tapp("vector",[TA_nexp base; TA_nexp rise; TA_ord o; TA_typ bit_t])}), + External (Some f),[],ef,ef,b_env)) in E_aux(E_app((Id_aux((Id f),l)), - [(E_aux (E_internal_exp(tannot), tannot));]),tannot),[],ef + [(E_aux (E_internal_exp(internal_tannot), tannot));]),tannot),[],ef | _ -> simp_exp e l (new_t ()),[],ef)) in let t',cs',_,e' = type_coerce (Expr l) d_env Require false true b_env (get_e_typ e) e expect_t in (e',t',t_env,cs@cs',nob,effect) @@ -775,15 +777,15 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): (match t_p.t with | Tfn(arg,ret,_,ef') -> check_parms arg lft rht | _ -> typ_error l ("Expected a function, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in - let _ = Printf.eprintf "Looking for overloaded function %s, generic type is %s, arg_t is %s\n" - i (t_to_string t_p) (t_to_string arg_t) in + (*let _ = Printf.eprintf "Looking for overloaded function %s, generic type is %s, arg_t is %s\n" + i (t_to_string t_p) (t_to_string arg_t) in*) (match (select_overload_variant d_env true overload_return variants arg_t) with | [] -> typ_error l ("No function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t)) | [Base((params,t),tag,cs,ef,_,b)] -> - let _ = Printf.eprintf "Selected an overloaded function for %s, - variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in + (*let _ = Printf.eprintf "Selected an overloaded function for %s, + variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*) (match t.t with | Tfn(arg,ret,imp,ef') -> (match arg.t,arg_t.t with @@ -795,15 +797,15 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): |_ -> raise (Reporting_basic.err_unreachable l "function no longer has tuple type")) | _ -> raise (Reporting_basic.err_unreachable l "overload variant does not have function")) | variants -> - let _ = Printf.eprintf "Number of variants found before looking at return value %i\n%!" - (List.length variants) in + (*let _ = Printf.eprintf "Number of variants found before looking at return value %i\n%!" + (List.length variants) in*) (match (select_overload_variant d_env false true variants expect_t) with | [] -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t) ^ " returning " ^ (t_to_string expect_t)) | [Base((params,t),tag,cs,ef,_,b)] -> - let _ = Printf.eprintf "Selected an overloaded function for %s, - variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in + (*let _ = Printf.eprintf "Selected an overloaded function for %s, + variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*) (match t.t with | Tfn(arg,ret,imp,ef') -> (match arg.t,arg_t.t with @@ -943,7 +945,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | (Def_val_empty,false) -> (Def_val_aux(Def_val_empty,(ld,simple_annot item_t)),true,[],pure_e) | (Def_val_empty,true) -> let ef = add_effect (BE_aux(BE_unspec,l)) pure_e in - let (de,_,_,_,_,ef_d) = check_exp envs imp_param item_t (E_aux(E_lit (L_aux(L_undef,l)), (l,NoTyp))) in + let de = E_aux(E_lit (L_aux(L_undef,l)), (l,simple_annot item_t)) in (Def_val_aux(Def_val_dec de, (l, cons_efs_annot item_t [] ef ef)),false,[],ef) | (Def_val_dec e,_) -> let (de,t,_,cs_d,_,ef_d) = (check_exp envs imp_param item_t e) in (*Check that ef_d doesn't write to memory or registers? *) @@ -1292,6 +1294,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): (E_aux(E_let(lb',e),(l,simple_annot_efr t effects)),t,t_env,cs@cs',nob,effects) | E_assign(lexp,exp) -> let (lexp',t',_,t_env',tag,cs,b_env',efl,efr) = check_lexp envs imp_param true lexp in + let t' = match t'.t with | Tapp("reg",[TA_typ t]) | Tapp("register",[TA_typ t]) + | Tabbrev(_,{t=Tapp("register",[TA_typ t])}) -> t + | _ -> t' in let (exp',t'',_,cs',_,efr') = check_exp envs imp_param t' exp in let (t',c') = type_consistent (Expr l) d_env Require false unit_t expect_t in let effects = union_effects efl (union_effects efr efr') in @@ -1843,8 +1848,8 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let check t_env tp_env imp_param = List.split (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) -> - let _ = Printf.eprintf "checking function %s : %s -> %s\n" - (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in + (*let _ = Printf.eprintf "checking function %s : %s -> %s\n" + (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) let (pat',t_env',cs_p,b_env',t') = check_pattern (Env(d_env,t_env,b_env,tp_env)) Emp_local param_t pat in let _, _ = type_consistent (Patt l) d_env Require false param_t t' in let exp',_,_,cs_e,_,ef = diff --git a/src/type_internal.ml b/src/type_internal.ml index 660ef20a..2fb06ce0 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -467,9 +467,11 @@ let rec pow_i i n = 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("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"}) -> true + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) | Tapp("reg",[TA_typ {t=Tid "bit"}]) -> true | _ -> false) | _ -> false @@ -2767,10 +2769,10 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> let cs = [Eq(co,b2,n_zero);LtEq(co,Guarantee,mk_sub (mk_2n(r1)) n_one,r2)] in - (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num",l)),[e]), + (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "unsigned",l)),[e]), (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))))) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> - eq_error l "Cannot convert a vector to an range without an order" + eq_error l "Cannot convert a vector to a range without an order" | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> eq_error l "Cannot convert non-bit vector into an range" | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded")) @@ -2779,7 +2781,7 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}], [TA_nexp b2] -> let cs = [GtEq(co,Guarantee,b2,n_zero);LtEq(co,Guarantee,b2,mk_sub (mk_2n(r1)) n_one)] in - (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num",l)),[e]), + (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "unsigned",l)),[e]), (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))))) | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> eq_error l "Cannot convert non-bit vector into an range" |