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/value.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/value.ml') diff --git a/src/value.ml b/src/value.ml index 157c16fc..589e956a 100644 --- a/src/value.ml +++ b/src/value.ml @@ -86,6 +86,12 @@ type value = | V_ref of string | V_ctor of string * value list | V_record of value StringMap.t + (* When constant folding we disable reading registers, so a register + read will return a V_attempted_read value. If we try to do + anything with this value, we'll get an exception - but if all we + do is return it then we can replace the expression we are folding + with a direct register read. *) + | V_attempted_read of string let rec eq_value v1 v2 = match v1, v2 with @@ -386,6 +392,7 @@ let rec string_of_value = function | V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" | V_record record -> "{" ^ Util.string_of_list ", " (fun (field, v) -> field ^ "=" ^ string_of_value v) (StringMap.bindings record) ^ "}" + | V_attempted_read _ -> assert false let value_sign_extend = function | [v1; v2] -> mk_vector (Sail_lib.sign_extend (coerce_bv v1, coerce_int v2)) -- cgit v1.2.3