summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/gen_lib/sail_values.lem18
-rw-r--r--src/gen_lib/vector.lem6
-rw-r--r--src/pretty_print.ml89
-rw-r--r--src/rewriter.ml48
4 files changed, 117 insertions, 44 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 4d74976b..33b8444e 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -3,16 +3,18 @@ open import State
open import Vector
open import Arch
+type i = integer
+
let length l = integerFromNat (length l)
-let has_undef (V bs _ _) = List.any (function U -> true | _ -> false end) bs
+let has_undef (V bs _ _) = List.any (function Undef -> true | _ -> false end) bs
let most_significant (V bs _ _) = let (b :: _) = bs in b
let bitwise_not_bit = function
| I -> O
| O -> I
- | _ -> U
+ | _ -> Undef
end
let (~) = bitwise_not_bit
@@ -23,8 +25,8 @@ let bitwise_not (V bs start is_inc) =
let bool_to_bit b = if b then I else O
let bitwise_binop_bit op = function
- | (U,_) -> U (*Do we want to do this or to respect | of I and & of B0 rules?*)
- | (_,U) -> U (*Do we want to do this or to respect | of I and & of B0 rules?*)
+ | (Undef,_) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
+ | (_,Undef) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
| (x,y) -> bool_to_bit (op (to_bool x) (to_bool y))
end
@@ -131,7 +133,7 @@ let to_vec_inc = to_vec true
let to_vec_dec = to_vec false
let to_vec_undef is_inc (len : integer) =
- V (replicate (natFromInteger len) U) (if is_inc then 0 else len-1) is_inc
+ V (replicate (natFromInteger len) Undef) (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
@@ -289,7 +291,7 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size (((V _ s
end in
if representable
then to_vec is_inc (act_size,n')
- else V (List.replicate (natFromInteger act_size) U) start is_inc
+ else V (List.replicate (natFromInteger act_size) Undef) start is_inc
let mod_vec = arith_op_vec_no0 integerMod false 1
let quot_vec = arith_op_vec_no0 integerDiv false 1
@@ -313,8 +315,8 @@ let arith_op_overflow_no0_vec op sign size (((V _ start is_inc) as l),r) =
if representable then
(to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
else
- (V (List.replicate (natFromInteger act_size) U) start is_inc,
- V (List.replicate (natFromInteger (act_size + 1)) U) start is_inc) in
+ (V (List.replicate (natFromInteger act_size) Undef) start is_inc,
+ V (List.replicate (natFromInteger (act_size + 1)) Undef) start is_inc) in
let overflow = if representable then O else I in
(correct_size_num,overflow,most_significant one_more)
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index 5e78e010..9efae768 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -1,6 +1,6 @@
open import Pervasives
-type bit = O | I | U
+type bit = O | I | Undef
type vector 'a = V of list 'a * integer * bool
let rec nth xs (n : integer) = match (n,xs) with
@@ -28,11 +28,11 @@ let make_indexed_vector_reg entries default start length =
V (List.foldl replace (replicate length v) entries) start
let make_indexed_vector_bit entries default start length =
- let default = match default with Nothing -> U | Just v -> v end in
+ let default = match default with Nothing -> Undef | Just v -> v end in
V (List.foldl replace (replicate length default) entries) start
let make_bitvector_undef length =
- V (replicate length U) 0 true
+ V (replicate length Undef) 0 true
let vector_concat (V bs start is_inc) (V bs' _ _) =
V (bs ++ bs') start is_inc
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 02fc62a5..6b1b364a 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1886,11 +1886,11 @@ let doc_lit_lem in_pat (L_aux(l,_)) =
| L_true -> "I"
| L_num i ->
let ipp = string_of_int i in
- (if i < 0 then "((0"^ipp^") : integer)"
- else "("^ipp^" : integer)")
+ (if i < 0 then "((0"^ipp^") : i)"
+ else "("^ipp^" : i)")
| L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*)
| L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*)
- | L_undef -> "U"
+ | L_undef -> "Undef"
| L_string s -> "\"" ^ s ^ "\"")
(* typ_doc is the doc for the type being quantified *)
@@ -2012,22 +2012,35 @@ let doc_exp_lem, doc_let_lem =
| E_app(f,args) ->
(match f with
(* temporary hack to make the loop body a function of the temporary variables *)
- | Id_aux ((Id (("foreach_inc" | "foreach_dec") as loopf),_)) ->
+ | Id_aux ((Id (("foreach_inc" | "foreach_dec" |
+ "foreachM_inc" | "foreachM_dec" ) as loopf),_)) ->
let call = doc_id_lem in
- let [id;indices;body;E_aux (E_tuple vars,_) as e5] = args in
- let vars = List.map (fun (E_aux (E_id (Id_aux (Id name,_)),_)) -> string name) vars in
- let varspp =
- match vars with
- | [v] -> v
- | _ -> parens (separate comma vars) in
- (prefix 2 1)
- (parens ((separate space) [string loopf;exp indices;exp e5]))
- (parens
- ((prefix 1 1)
- (separate space [string "fun";exp id;varspp;arrow])
- (exp body)
- )
- )
+ let [id;indices;body;e5] = args in
+ (match e5 with
+ | E_aux (E_tuple vars,_) ->
+ let vars = List.map (fun (E_aux (E_id (Id_aux (Id name,_)),_)) -> string name) vars in
+ let varspp =
+ match vars with
+ | [v] -> v
+ | _ -> parens (separate comma vars) in
+ (prefix 2 1)
+ (parens ((separate space) [string loopf;exp indices;exp e5]))
+ (parens
+ ((prefix 1 1)
+ (separate space [string "fun";exp id;varspp;arrow])
+ (top_exp false body)
+ )
+ )
+ | E_aux (E_lit (L_aux (L_unit,_)),_) ->
+ (prefix 2 1)
+ (parens ((separate space) [string loopf;exp indices;exp e5]))
+ (parens
+ ((prefix 1 1)
+ (separate space [string "fun";exp id;string "_";arrow])
+ (top_exp false body)
+ )
+ )
+ )
| _ ->
(match annot with
| Base (_,Constructor _,_,_,_,_) ->
@@ -2416,31 +2429,44 @@ let reg_decls (Defs defs) =
[],[]) in
let regs_pp =
- (prefix 2 1)
- (separate space [string "type";string "register";equals])
- ((separate_map space (fun (reg,_) -> pipe ^^ space ^^ string reg) regs)
- ^^ space ^^ pipe ^^ space ^^ string "UndefinedReg of integer" ^^
- pipe ^^ space ^^ string "RegisterPair of register * register") in
+ if regs = [] then
+ string "type register = NO_REGISTERS"
+ else
+ (prefix 2 1)
+ (separate space [string "type";string "register";equals])
+ ((separate_map space (fun (reg,_) -> pipe ^^ space ^^ string reg) regs)
+ ^^ space ^^ pipe ^^ space ^^ string "UndefinedReg of integer" ^^
+ pipe ^^ space ^^ string "RegisterPair of register * register") in
let regfields_pp =
+ if rsranges = [] then
+ string "type register_field = | NO_REGISTER_FIELDS"
+ else
(prefix 2 1)
(separate space [string "type";string "register_field";equals])
(separate_map space (fun (fname,tname,_,_) ->
pipe ^^ space ^^ string (tname ^ "_" ^ fname)) rsranges) in
let regfieldsbit_pp =
+ if rsbits = [] then
+ string "type register_field_bit = | NO_REGISTER_FIELD_BITS"
+ else
(prefix 2 1)
(separate space [string "type";string "register_field_bit";equals])
(separate_map space (fun (fname,tname,_) ->
pipe ^^ space ^^ string (tname ^ "_" ^ fname)) rsbits) in
let regalias_pp =
+ if regaliases = [] then empty else
(separate_map (break 1))
(fun (name1,(name2,name3)) ->
separate space [string "let";string name1;equals;string "RegisterPair";string name2;string name3])
regaliases in
let state_pp =
+ if regs = [] then
+ string "type state = EMPTY_STATE"
+ else
(prefix 2 1)
(separate space [string "type";string "state";equals])
(anglebars
@@ -2450,6 +2476,9 @@ let reg_decls (Defs defs) =
)) in
let length_pp =
+ if regs = [] then
+ string "length_reg _ = (0 : integer)"
+ else
(separate space [string "val";string "length_reg";colon;string "register";arrow;string "integer"])
^/^
(prefix 2 1)
@@ -2471,6 +2500,9 @@ let reg_decls (Defs defs) =
let field_indices_pp =
+ if rsranges = [] then
+ string "let field_indices _ = ((0 : integer),(0 : integer))"
+ else
(prefix 2 1)
((separate space) [string "let";string "field_indices";
colon;string "register_field";arrow;string "(integer * integer)";
@@ -2485,7 +2517,10 @@ let reg_decls (Defs defs) =
) ^/^ string "end" ^^ hardline
) in
-let field_index_bit_pp =
+ let field_index_bit_pp =
+ if rsbits = [] then
+ string "let field_index_bit _ = (0 : integer)"
+ else
(prefix 2 1)
((separate space) [string "let";string "field_index_bit";
colon;string "register_field_bit";arrow;string "integer";
@@ -2501,6 +2536,9 @@ let field_index_bit_pp =
let read_regstate_pp =
+ if regs = [] then
+ string "let read_regstate _ _ -> Vector 0 0 true"
+ else
(prefix 2 1)
(separate space [string "let rec";string "read_regstate";string "s";equals;string "function"])
(
@@ -2515,6 +2553,9 @@ let field_index_bit_pp =
string "end" ^^ hardline ) in
let write_regstate_pp =
+ if regs = [] then
+ string "let write_regstate _ _ _ -> EMPTY_STATE"
+ else
(prefix 2 1)
(separate space [string "let rec";string "write_regstate";string "s";string "reg";string "v";
equals;string "match reg with"])
diff --git a/src/rewriter.ml b/src/rewriter.ml
index c7e6986b..1761bcc5 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -24,6 +24,8 @@ let fresh_name () =
let current = !fresh_name_counter in
let () = fresh_name_counter := (current + 1) in
current
+let reset_fresh_name_counter () =
+ fresh_name_counter := 0
let geteffs_annot (_,t) = match t with
| Base (_,_,_,_,effs,_) -> effs
@@ -344,7 +346,8 @@ let rewrite_lexp rewriters map (LEXP_aux(lexp,(l,annot))) =
| LEXP_field (lexp,id) -> rewrap (LEXP_field (rewriters.rewrite_lexp rewriters map lexp,id))
let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) =
- let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),(l,annot))) =
+ let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),(l,annot))) =
+ let _ = reset_fresh_name_counter () in
(*let _ = Printf.eprintf "Rewriting function %s, pattern %s\n"
(match id with (Id_aux (Id i,_)) -> i) (Pretty_print.pat_to_string pat) in*)
let map = get_map_tannot fdannot in
@@ -736,7 +739,11 @@ let remove_vector_concat_pat pat =
let subv = E_aux (E_vector_subrange (E_aux (E_id rootid,rannot),index i,index j),cannot) in
let typ = (Parse_ast.Unknown,simple_annot {t = Tid "unit"}) in
let letbind = LB_val_implicit (P_aux (P_id child,cannot),subv) in
- (LB_aux (letbind,typ), (fun body -> E_aux (E_let (LB_aux (letbind,cannot),body),typ))) in
+ let (Id_aux (Id rootname,_)) = rootid in
+ let (Id_aux (Id childname,_)) = child in
+ (LB_aux (letbind,typ),
+ (fun body -> E_aux (E_let (LB_aux (letbind,cannot),body),typ)),
+ (rootname,childname)) in
let p_aux = function
| ((P_as (P_aux (P_vector_concat pats,rannot'),rootid),decls),rannot) ->
@@ -747,12 +754,12 @@ let remove_vector_concat_pat pat =
(* if we see a named vector pattern, remove the name and remember to
declare it later *)
| P_as (P_aux (p,cannot),cname) ->
- let (lb,decl) = letbind_vec (rootid,rannot) (cname,cannot) (pos,pos + length - 1) in
- (pos + length, pat_acc @ [P_aux (p,cannot)], decl_acc @ [(lb,decl)])
+ let (lb,decl,info) = letbind_vec (rootid,rannot) (cname,cannot) (pos,pos + length - 1) in
+ (pos + length, pat_acc @ [P_aux (p,cannot)], decl_acc @ [((lb,decl),info)])
(* if we see a P_id variable, remember to declare it later *)
| P_id cname ->
- let (lb,decl) = letbind_vec (rootid,rannot) (cname,cannot) (pos,pos + length - 1) in
- (pos + length, pat_acc @ [P_aux (P_id cname,cannot)], decl_acc @ [(lb,decl)])
+ let (lb,decl,info) = letbind_vec (rootid,rannot) (cname,cannot) (pos,pos + length - 1) in
+ (pos + length, pat_acc @ [P_aux (P_id cname,cannot)], decl_acc @ [((lb,decl),info)])
(* normal vector patterns are fine *)
| _ -> (pos + length, pat_acc @ [P_aux (p,cannot)],decl_acc) )
(* non-vector patterns aren't *)
@@ -792,7 +799,30 @@ let remove_vector_concat_pat pat =
let (pat,decls) = fold_pat unname_vector_concat_elements pat in
- let (letbinds,decls) = List.split decls in
+ let decls =
+ let module S = Set.Make(String) in
+
+ let roots_needed =
+ List.fold_right
+ (fun (_,(rootid,childid)) roots_needed ->
+ if S.mem childid roots_needed then
+ (* let _ = print_endline rootid in *)
+ S.add rootid roots_needed
+ else if String.length childid >= 3 && String.sub childid 0 2 = String.sub "__v" 0 2 then
+ roots_needed
+ else
+ S.add rootid roots_needed
+ ) decls S.empty in
+ List.filter
+ (fun (_,(_,childid)) ->
+ S.mem childid roots_needed ||
+ String.length childid < 3 ||
+ not (String.sub childid 0 2 = String.sub "__v" 0 2))
+ decls in
+
+ let (letbinds,decls) =
+ let (decls,_) = List.split decls in
+ List.split decls in
let decls = List.fold_left (fun f g x -> f (g x)) (fun b -> b) decls in
@@ -1315,7 +1345,7 @@ and n_exp (exp : 'a exp) (k : 'a exp -> 'a exp) : 'a exp =
| E_internal_plet _ -> failwith "E_internal_plet should not be here yet"
-let rewrite_defs_a_normalise =
+let rewrite_defs_a_normalise =
let rewrite_exp _ _ e =
let e = remove_blocks e in
n_exp_term (effectful e) e in
@@ -1325,7 +1355,7 @@ let rewrite_defs_a_normalise =
; rewrite_let = rewrite_let
; rewrite_lexp = rewrite_lexp
; rewrite_fun = rewrite_fun
- ; rewrite_def = rewrite_def
+ ; rewrite_def = (fun rws def -> let _ = reset_fresh_name_counter () in rewrite_def rws def)
; rewrite_defs = rewrite_defs_base
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 23:29:30 +0000