Allow folding constant expressions into single register reads

Essentially all we have to do to make this work is introduce a member of
the Value type, V_attempted_read <reg>, which is returned whenever we
try to read a register value with allow_registers disabled. This defers
the failure from reading the register to the point where the register
value is used (simply because nothing knows how to deal with
V_attempted_read). However, if V_attempted_read is returned directly as
the result of evaluating an expression, then we can replace the
expression with a single direct register read. This optimises some
indirection in the ARM specification.

1 files changed, 3 insertions, 1 deletions

diff --git a/src/interpreter.ml b/src/interpreter.ml
index 07a4b4ae..03877600 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -390,13 +390,15 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
                Type_check.check_exp (env_of_annot annot) exp (typ_of orig_exp)
           in
           return exp
+       | Register _ when not gstate.allow_registers ->
+          return (exp_of_value (V_attempted_read (string_of_id id)))
        | Local (Mutable, _) -> return (local_variable id lstate gstate)
        | Local (Immutable, _) ->
           let chain = build_letchain id gstate.letbinds orig_exp in
           return chain
        | Enum _ ->
           return (exp_of_value (V_ctor (string_of_id id, [])))
-       | _ -> failwith ("Coudln't find id " ^ string_of_id id)
+       | _ -> failwith ("Couldn't find id " ^ string_of_id id)
      end
 
   | E_record (FES_aux (FES_Fexps (fexps, flag), fes_annot)) ->