From e3aa6935bfe7bb1e92a5c70f3df4bd380149d03c Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Sat, 20 Apr 2019 11:58:53 +0100 Subject: Fix: Reduce constant-fold time for ARM from 20min+ to 10s With the new interpreter changes computing the initial state for the interpreter does some significant work. The existing code was re-computing the initial state for every subexpression in the specification (not even just the ones due to be constant-folded away). Now we just compute the initial state once and use it for all constant folds. Also reduce the time taken for the simple_assignments rewrite from 20s to under 1s for ARMv8.5, by skipping l-expressions that are already in the simplest form. --- src/constant_fold.ml | 3 ++- src/rewrites.ml | 4 ++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/constant_fold.ml b/src/constant_fold.ml index 14d6550c..f2e0add5 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -251,10 +251,11 @@ let rec rewrite_constant_function_calls' ast = let rewrite_count = ref 0 in let ok () = incr rewrite_count in let not_ok () = decr rewrite_count in + let istate = initial_state ast Type_check.initial_env in let rw_defs = { rewriters_base with - rewrite_exp = (fun _ -> rw_exp ok not_ok (initial_state ast Type_check.initial_env)) + rewrite_exp = (fun _ -> rw_exp ok not_ok istate) } in let ast = rewrite_defs_base rw_defs ast in (* We keep iterating until we have no more re-writes to do *) diff --git a/src/rewrites.ml b/src/rewrites.ml index 34d45618..a37449a4 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2153,6 +2153,10 @@ let rewrite_simple_assignments env defs = let assign_e_aux e_aux annot = let env = env_of_annot annot in match e_aux with + | E_assign (LEXP_aux (LEXP_id _, _), _) -> + E_aux (e_aux, annot) + | E_assign (LEXP_aux (LEXP_cast (_, _), _), _) -> + E_aux (e_aux, annot) | E_assign (lexp, exp) -> let (lexp, rhs) = rewrite_lexp_to_rhs lexp in let assign = mk_exp (E_assign (strip_lexp lexp, strip_exp (rhs exp))) in -- cgit v1.2.3