From 3a0bcd6e7f1dd565fb41574285c9c09bbbe14697 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 28 Nov 2018 00:29:10 +0000 Subject: 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 , 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. --- src/interpreter.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/interpreter.ml') 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)) -> -- cgit v1.2.3