summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/gen_lib/sail_values.lem4
-rw-r--r--src/pretty_print.ml65
-rw-r--r--src/rewriter.ml95
3 files changed, 80 insertions, 84 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 2681d334..d2364397 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -466,3 +466,7 @@ let make_bitvector_undef length =
let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n)
+
+let mask (n,V bits start dir) =
+ let current_size = List.length bits in
+ V (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 1d2c89f3..546fc770 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1864,18 +1864,19 @@ let doc_typ_lem, doc_atomic_typ_lem =
(doc_id_lem_type id) ^^ space ^^ (separate_map space doc_typ_arg_lem args)
| _ -> atomic_typ ty
and atomic_typ ((Typ_aux (t, _)) as ty) = match t with
- | Typ_id id -> doc_id_lem_type id
- | Typ_var v -> doc_var v
- | Typ_wild -> underscore
- | Typ_app _ | Typ_tup _ | Typ_fn _ ->
- (* exhaustiveness matters here to avoid infinite loops
- * if we add a new Typ constructor *)
- group (parens (typ ty))
+ | Typ_id (Id_aux ((Id "bool"),_)) -> string "bit"
+ | Typ_id id -> doc_id_lem_type id
+ | Typ_var v -> doc_var v
+ | Typ_wild -> underscore
+ | Typ_app _ | Typ_tup _ | Typ_fn _ ->
+ (* exhaustiveness matters here to avoid infinite loops
+ * if we add a new Typ constructor *)
+ group (parens (typ ty))
and doc_typ_arg_lem (Typ_arg_aux(t,_)) = match t with
- | Typ_arg_typ t -> app_typ t
- | Typ_arg_nexp n -> empty
- | Typ_arg_order o -> empty
- | Typ_arg_effect e -> empty
+ | Typ_arg_typ t -> app_typ t
+ | Typ_arg_nexp n -> empty
+ | Typ_arg_order o -> empty
+ | Typ_arg_effect e -> empty
in typ, atomic_typ
let doc_lit_lem in_pat (L_aux(l,_)) =
@@ -1906,20 +1907,20 @@ let doc_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),_)) =
let rec doc_pat_lem apat_needed (P_aux (p,(l,annot)) as pa) = match p with
| P_app(id, ((_ :: _) as pats)) ->
(match annot with
- | Base(_,Constructor _,_,_,_,_) ->
+ | Base(_,(Constructor _ | Enum _),_,_,_,_) ->
let ppp = doc_unop (doc_id_lem_ctor true id)
- (separate_map space (doc_pat_lem true) pats) in
+ (parens (separate_map comma (doc_pat_lem true) pats)) in
if apat_needed then parens ppp else ppp
| _ -> empty)
+ | P_app(id,[]) ->
+ (match annot with
+ | Base(_,(Constructor _| Enum _),_,_,_,_) -> doc_id_lem_ctor apat_needed id
+ | _ -> empty)
| P_lit lit -> doc_lit_lem true lit
| P_wild -> underscore
| P_id id -> doc_id_lem id
| P_as(p,id) -> parens (separate space [doc_pat_lem true p; string "as"; doc_id_lem id])
| P_typ(typ,p) -> doc_op colon (doc_pat_lem true p) (doc_typ_lem typ)
- | P_app(id,[]) ->
- (match annot with
- | Base(_,Constructor n,_,_,_,_) -> doc_id_lem_ctor apat_needed id
- | _ -> empty)
| P_vector pats ->
let ppp =
(separate space)
@@ -1958,7 +1959,7 @@ let doc_exp_lem, doc_let_lem =
if t = Tid "bit" then
failwith "indexing a register's (single bit) bitfield not supported"
else
- let typprefix = String.uncapitalize (getregtyp le) ^ "_" in
+ let typprefix = getregtyp le ^ "_" in
(prefix 2 1)
(string "write_reg_field_range")
(align (doc_lexp_deref_lem le ^^ space ^^ string typprefix ^^
@@ -1974,7 +1975,7 @@ let doc_exp_lem, doc_let_lem =
if t = Tid "bit" then
failwith "indexing a register's (single bit) bitfield not supported"
else
- let typprefix = String.uncapitalize (getregtyp le) ^ "_" in
+ let typprefix = getregtyp le ^ "_" in
(prefix 2 1)
(string "write_reg_field_bit")
(align (doc_lexp_deref_lem le ^^ space ^^ string typprefix ^^
@@ -1985,13 +1986,13 @@ let doc_exp_lem, doc_let_lem =
(doc_lexp_deref_lem le ^^ space ^^ exp e2 ^/^ exp e)
)
| LEXP_field (le,id), (Tid "bit"| Tabbrev (_,{t=Tid "bit"})), _ ->
- let typprefix = String.uncapitalize (getregtyp le) ^ "_" in
+ let typprefix = getregtyp le ^ "_" in
(prefix 2 1)
(string "write_reg_bitfield")
(doc_lexp_deref_lem le ^^ space ^^ string typprefix ^^
doc_id_lem id ^/^ exp e)
| LEXP_field (le,id), _, _ ->
- let typprefix = String.uncapitalize (getregtyp le) ^ "_" in
+ let typprefix = getregtyp le ^ "_" in
(prefix 2 1)
(string "write_reg_field")
(doc_lexp_deref_lem le ^^ space ^^ string typprefix ^^
@@ -2005,7 +2006,7 @@ let doc_exp_lem, doc_let_lem =
| _ -> string "write_reg_bitfield" in
(prefix 2 1)
f
- (separate space [string reg;string (String.lowercase reg ^ "_" ^ field);exp e])
+ (separate space [string reg;string (reg ^ "_" ^ field);exp e])
(* the type should go instead of the lowercase reg *)
| Alias_pair(reg1,reg2) ->
string "write_two_regs" ^^ space ^^ string reg1 ^^ space ^^
@@ -2072,7 +2073,7 @@ let doc_exp_lem, doc_let_lem =
| _ ->
(match annot with
| Base (_,Constructor _,_,_,_,_) ->
- let epp = separate space [doc_id_lem f;separate_map space (top_exp true) args] in
+ let epp = doc_id_lem f ^^ space ^^ parens (separate_map comma (top_exp true) args) in
if aexp_needed then parens (align epp) else epp
| Base (_,External (Some "bitwise_not_bit"),_,_,_,_) ->
let [a] = args in
@@ -2142,12 +2143,12 @@ let doc_exp_lem, doc_let_lem =
| Tid "bit" | Tabbrev (_,{t=Tid "bit"}) ->
(separate space)
[string "read_reg_bitfield"; string reg;
- string (String.lowercase reg ^ "_" ^ field)]
+ string (reg ^ "_" ^ field)]
(* the type should go instead of the lowercase reg *)
| _ ->
(separate space)
[string "read_reg_field"; string reg;
- string (String.lowercase reg ^ "_" ^ field)] in
+ string (reg ^ "_" ^ field)] in
(* the type should go instead of the lowercase reg *)
if aexp_needed then parens (align epp) else epp
| Alias_pair(reg1,reg2) ->
@@ -2392,7 +2393,7 @@ let doc_exp_lem, doc_let_lem =
(*TODO Upcase and downcase type and constructors as needed*)
let doc_type_union_lem (Tu_aux(typ_u,_)) = match typ_u with
- | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor false id; string "of"; doc_typ_lem typ;]
+ | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor false id; string "of"; parens (doc_typ_lem typ)]
| Tu_id id -> separate space [pipe; doc_id_lem_ctor false id]
let rec doc_range_lem (BF_aux(r,_)) = match r with
@@ -2545,10 +2546,12 @@ let reg_decls (Defs defs) =
(prefix 2 1)
(separate space [string "let rec";string "length_reg";string "reg";equals;string "match reg with"])
(((separate_map (break 1))
- (fun (name,typ) ->
+ (fun (name,typ) ->
let ((n1,n2,_,_),typname) =
match typ with
- | Some typname -> (List.assoc typname regtypes,"register_" ^ typname)
+ | Some typname ->
+ (try (List.assoc typname regtypes,"register_" ^ typname) with
+ | Not_found -> failwith ("Couldn't find register type " ^ typname))
| None -> (default,"register") in
separate space [pipe;string name;arrow;doc_nexp (if is_inc then n2 else n1);
minus;doc_nexp (if is_inc then n1 else n2);plus;string "1"])
@@ -2740,10 +2743,10 @@ let reg_decls (Defs defs) =
string "let vsize = length v in";
string "let vsize = integerFromNat vsize in";
string ("let r1_v = slice v start " ^
- (if is_inc then "(size - start - 1) in" else "(start - size) - 1) in"));
+ (if is_inc then "(size - start - 1) in" else "(start - size - 1) in"));
string ("let r2_v = slice v " ^
- (if is_inc then "(size - start)" else "(start - size)") ^
- (if is_inc then "(vsize - start) in" else ("start - vsize) in")));
+ (if is_inc then "(size - start) " else "(start - size) ") ^
+ (if is_inc then "(vsize - start) in" else ("(start - vsize) in")));
string "write_regstate_aux (write_regstate_aux s r1 r1_v) r2 r2_v"
])) ^/^
string "end" ^^ hardline ) in
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 55c19a41..f920128a 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -44,18 +44,19 @@ let get_type_annot (_,t) = match t with
let get_type (E_aux (_,a)) = get_type_annot a
+let union_effs effs =
+ List.fold_left (fun acc eff -> union_effects acc eff) pure_e effs
+
let get_effsum_exp (E_aux (_,a)) = get_effsum_annot a
let get_effsum_fpat (FP_aux (_,a)) = get_effsum_annot a
let get_effsum_lexp (LEXP_aux (_,a)) = get_effsum_annot a
let get_effsum_fexp (FE_aux (_,a)) = get_effsum_annot a
-let get_effsum_fexps (FES_aux (_,a)) = get_effsum_annot a
+let get_effsum_fexps (FES_aux (FES_Fexps (fexps,_),_)) =
+ union_effs (List.map get_effsum_fexp fexps)
let get_effsum_opt_default (Def_val_aux (_,a)) = get_effsum_annot a
let get_effsum_pexp (Pat_aux (_,a)) = get_effsum_annot a
let get_effsum_lb (LB_aux (_,a)) = get_effsum_annot a
-let union_effs effs =
- List.fold_left (fun acc eff -> union_effects acc eff) pure_e effs
-
let eff_union_exps es =
union_effs (List.map get_effsum_exp es)
@@ -117,14 +118,7 @@ let fix_effsum_fexp (FE_aux (fexp,(l,annot))) =
| FE_Fexp (_,e) -> get_effsum_exp e in
FE_aux (fexp,(l,(Base (t,tag,nexps,eff,union_effects eff effsum,bounds))))
-let fix_effsum_fexps (FES_aux (fexps,(l,annot))) =
- match annot with
- | NoTyp ->
- raise ((Reporting_basic.err_unreachable l) ("fix_effsum_fexps missing type information"))
- | Base (t,tag,nexps,eff,_,bounds) ->
- let effsum = match fexps with
- | FES_Fexps (fexps,_) -> union_effs (List.map get_effsum_fexp fexps) in
- FES_aux (fexps,(l,(Base (t,tag,nexps,eff,union_effects eff effsum,bounds))))
+let fix_effsum_fexps fexps = fexps (* FES_aux have no effect information *)
let fix_effsum_opt_default (Def_val_aux (opt_default,(l,annot))) =
let (Base (t,tag,nexps,eff,_,bounds)) = annot in
@@ -745,33 +739,18 @@ let id_exp_alg =
let remove_vector_concat_pat pat =
- (* ivc: bool that indicates whether the exp is in a vector_concat pattern *)
- let remove_tannot_in_vector_concats =
- { p_lit = (fun lit ivc -> P_lit lit)
- ; p_wild = (fun ivc -> P_wild)
- ; p_as = (fun (pat,id) ivc -> P_as (pat ivc,id))
- ; p_typ =
- (fun (typ,pat) ivc ->
- let P_aux (p,annot) = pat ivc in
- if ivc then p else P_typ (typ,P_aux (p,annot))
- )
- ; p_id = (fun id ivc -> P_id id)
- ; p_app = (fun (id,ps) ivc -> P_app (id, List.map (fun p -> p ivc) ps))
- ; p_record =
- (fun (fpats,b) ivc -> P_record (List.map (fun f -> f false) fpats, b))
- ; p_vector = (fun ps ivc -> P_vector (List.map (fun p -> p ivc) ps))
- ; p_vector_indexed =
- (fun ps ivc -> P_vector_indexed (List.map (fun (i,p) -> (i,p ivc)) ps))
- ; p_vector_concat =
- (fun ps ivc -> P_vector_concat (List.map (fun p -> p true) ps))
- ; p_tup = (fun ps ivc -> P_tup (List.map (fun p -> p ivc) ps))
- ; p_list = (fun ps ivc -> P_list (List.map (fun p -> p ivc) ps))
- ; p_aux = (fun (p,annot) ivc -> P_aux (p ivc,annot))
- ; fP_aux = (fun (fpat,annot) ivc -> FP_aux (fpat false,annot))
- ; fP_Fpat = (fun (id,p) ivc -> FP_Fpat (id,p false))
- } in
- let pat = (fold_pat remove_tannot_in_vector_concats pat) false in
+ (* ivc: bool that indicates whether the exp is in a vector_concat pattern *)
+ let remove_typed_patterns =
+ fold_pat { id_pat_alg with
+ p_aux = (function
+ | (P_typ (_,P_aux (p,_)),annot)
+ | (p,annot) ->
+ P_aux (p,annot)
+ )
+ } in
+
+ let pat = remove_typed_patterns pat in
let fresh_name l =
let current = fresh_name () in
@@ -784,9 +763,9 @@ let remove_vector_concat_pat pat =
(* introduce names for all patterns of form P_vector_concat *)
let name_vector_concat_roots =
{ p_lit = (fun lit -> P_lit lit)
+ ; p_typ = (fun (typ,p) -> P_typ (typ,p false)) (* cannot happen *)
; p_wild = P_wild
; p_as = (fun (pat,id) -> P_as (pat true,id))
- ; p_typ = (fun (typ,pat) -> P_typ (typ,pat false))
; p_id = (fun id -> P_id id)
; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps))
; p_record = (fun (fpats,b) -> P_record (fpats, b))
@@ -797,17 +776,16 @@ let remove_vector_concat_pat pat =
; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps))
; p_aux =
(fun (pat,((l,_) as annot)) contained_in_p_as ->
- match pat with
- | P_vector_concat pats ->
- (if contained_in_p_as
- then P_aux (pat,annot)
- else P_aux (P_as (P_aux (pat,annot),fresh_name l),annot))
- | _ -> P_aux (pat,annot)
+ match pat with
+ | P_vector_concat pats ->
+ (if contained_in_p_as
+ then P_aux (pat,annot)
+ else P_aux (P_as (P_aux (pat,annot),fresh_name l),annot))
+ | _ -> P_aux (pat,annot)
)
; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot))
; fP_Fpat = (fun (id,p) -> FP_Fpat (id,p false))
} in
-
let pat = (fold_pat name_vector_concat_roots pat) false in
@@ -816,8 +794,12 @@ let remove_vector_concat_pat pat =
let p_vector_concat pats =
let aux ((P_aux (p,((l,_) as a))) as pat) = match p with
| P_vector _ -> P_aux (P_as (pat,fresh_name l),a)
- (* | P_vector_concat. cannot happen after folding function name_vector_concat_roots *)
- | _ -> pat in (* this can only be P_as and P_id *)
+ | P_id id -> P_aux (P_id id,a)
+ | P_as (p,id) -> P_aux (P_as (p,id),a)
+ | _ ->
+ raise
+ (Reporting_basic.err_unreachable
+ l "name_vector_concat_elements: Non-vector in vector-concat pattern") in
P_vector_concat (List.map aux pats) in
{id_pat_alg with p_vector_concat = p_vector_concat} in
@@ -851,7 +833,8 @@ let remove_vector_concat_pat pat =
let p_aux = function
| ((P_as (P_aux (P_vector_concat pats,rannot'),rootid),decls),rannot) ->
let aux (pos,pat_acc,decl_acc) (P_aux (p,cannot)) = match cannot with
- | (_,Base((_,{t = Tapp ("vector",[_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_)) ->
+ | (_,Base((_,{t = Tapp ("vector",[_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_))
+ | (_,Base((_,{t = Tabbrev (_,{t = Tapp ("vector",[_;TA_nexp {nexp = Nconst length};_;_])})}),_,_,_,_,_)) ->
let length = int_of_big_int length in
(match p with
(* if we see a named vector pattern, remove the name and remember to
@@ -866,10 +849,12 @@ let remove_vector_concat_pat pat =
(* normal vector patterns are fine *)
| _ -> (pos + length, pat_acc @ [P_aux (p,cannot)],decl_acc) )
(* non-vector patterns aren't *)
- | (l,_) ->
+ | (l,Base((_,t),_,_,_,_,_)) ->
raise
(Reporting_basic.err_unreachable
- l "unname_vector_concat_elements: Non-vector in vector-concat pattern") in
+ l ("unname_vector_concat_elements: Non-vector in vector-concat pattern:" ^
+ t_to_string t)
+ ) in
let (_,pats',decls') = List.fold_left aux (0,[],[]) pats in
(P_aux (P_as (P_aux (P_vector_concat pats',rannot'),rootid),rannot), decls @ decls')
| ((p,decls),annot) -> (P_aux (p,annot),decls) in
@@ -957,11 +942,15 @@ let remove_vector_concat_pat pat =
match p,annot with
| P_vector ps,_ -> acc @ ps
| P_id _,
- (_,Base((_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_)) ->
+ (_,Base((_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_))
+ | P_id _,
+ (_,Base((_,{t = Tabbrev (_,{t = Tapp ("vector",[_;TA_nexp {nexp = Nconst length};_;_])})}),_,_,_,_,_)) ->
let wild _ = P_aux (P_wild,(Parse_ast.Generated l,simple_annot {t = Tid "bit"})) in
acc @ (List.map wild (range 0 ((int_of_big_int length) - 1)))
| P_wild,
- (_,Base((_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_)) ->
+ (_,Base((_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_))
+ | P_wild,
+ (_,Base((_,{t = Tabbrev (_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])})}),_,_,_,_,_)) ->
let wild _ = P_aux (P_wild,(Parse_ast.Generated l,simple_annot {t = Tid "bit"})) in
acc @ (List.map wild (range 0 ((int_of_big_int length) - 1)))
| P_lit _,(l,_) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 21:11:32 +0000