diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/constant_fold.ml | 1 | ||||
| -rw-r--r-- | src/interpreter.ml | 4 | ||||
| -rw-r--r-- | src/value.ml | 7 |
3 files changed, 11 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)) |