diff options
| author | Alasdair Armstrong | 2019-04-20 11:58:53 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-04-20 12:06:40 +0100 |
| commit | e3aa6935bfe7bb1e92a5c70f3df4bd380149d03c (patch) | |
| tree | 209c3a7c6151e9d6d753f3fd079972d3891b4fda /src/rewrites.ml | |
| parent | d2b4e990d915a121c59cf58f2ea7a89348c0d55c (diff) | |
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.
Diffstat (limited to 'src/rewrites.ml')
| -rw-r--r-- | src/rewrites.ml | 4 |
1 files changed, 4 insertions, 0 deletions
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 |