From 9cfa575245a0427a0d35504086de182bd80b7df8 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 11 Jan 2019 21:00:36 +0000 Subject: Updates for sail-arm release We want to ensure that no_devices.sail and devices.sail have the same effect footprint, because with a snapshot-type release in sail-arm, we can't rebuild the spec with asl_to_sail every time we switch from running elf binaries to booting OS's. This commit allows registers to have arbitrary effects, so registers that are really representing memory-mapped devices don't have to have the wmem/rmem effect. --- src/rewriter.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'src/rewriter.ml') diff --git a/src/rewriter.ml b/src/rewriter.ml index 39b437f4..03c0e074 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -366,11 +366,20 @@ let rewrite_def rewriters d = match d with | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewriter") let rewrite_defs_base rewriters (Defs defs) = + let rec rewrite = function + | [] -> [] + | d :: ds -> + let d = rewriters.rewrite_def rewriters d in + d :: rewrite ds + in + Defs (rewrite defs) + +let rewrite_defs_base_progress prefix rewriters (Defs defs) = let total = List.length defs in let rec rewrite n = function | [] -> [] | d :: ds -> - if !Profile.opt_profile then Util.progress n total else (); + Util.progress (prefix ^ " ") (string_of_int n ^ "/" ^ string_of_int total) n total; let d = rewriters.rewrite_def rewriters d in d :: rewrite (n + 1) ds in -- cgit v1.2.3