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.

5 files changed, 42 insertions, 1 deletions

diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index f22b48de..0e34ed5b 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -78,6 +78,7 @@ and exp_of_value =
   | V_tuple vs ->
      mk_exp (E_tuple (List.map exp_of_value vs))
   | V_unit -> mk_lit_exp L_unit
+  | V_attempted_read str -> mk_exp (E_id (mk_id str))
   | _ -> failwith "No expression for value"
 
 (* We want to avoid evaluating things like print statements at compile
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)) ->
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))
diff --git a/test/c/cfold_reg.expect b/test/c/cfold_reg.expect
new file mode 100644
index 00000000..27ba77dd
--- /dev/null
+++ b/test/c/cfold_reg.expect
@@ -0,0 +1 @@
+true
diff --git a/test/c/cfold_reg.sail b/test/c/cfold_reg.sail
new file mode 100644
index 00000000..a5090e91
--- /dev/null
+++ b/test/c/cfold_reg.sail
@@ -0,0 +1,30 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "eq_string" : (string, string) -> bool
+
+overload operator == = {eq_string}
+
+register R : bool
+
+val "print_endline" : string -> unit
+
+function IMPDEF(str : string) -> bool = {
+  if str == "A" then {
+    return(R)
+  } else if str == "B" then {
+    true
+  } else {
+    false
+  }
+}
+
+function main(() : unit) -> unit = {
+  R = true;
+  if IMPDEF("A") then {
+    print_endline("true")
+  } else {
+    print_endline("false")
+  }
+}
\ No newline at end of file