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/rewrites.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/rewrites.ml')

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