diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/bitfield.ml | 1 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 2 | ||||
| -rw-r--r-- | src/rewrites.ml | 7 |
3 files changed, 8 insertions, 2 deletions
diff --git a/src/bitfield.ml b/src/bitfield.ml index db3411b1..67a26b89 100644 --- a/src/bitfield.ml +++ b/src/bitfield.ml @@ -101,6 +101,7 @@ let index_range_getter' name field order start stop = let index_range_setter' name field order start stop = let size = if start > stop then start - (stop - 1) else stop - (start - 1) in let irs_val = Printf.sprintf "val _set_%s : (register(%s), %s) -> unit effect {wreg}" field name (bitvec size order) in + (* Read-modify-write using an internal _reg_deref function without rreg effect *) let irs_function = String.concat "\n" [ Printf.sprintf "function _set_%s (r_ref, v) = {" field; Printf.sprintf " r = _get_%s(_reg_deref(r_ref));" name; diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index df530bc7..b6852aaf 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -182,7 +182,7 @@ let write_tag t state = let tagstate = Map.insert taddr t state.tagstate in [(Value true, <| state with tagstate = tagstate |>)] -val read_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> M 'regs 'a 'e +val read_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> M 'regs 'a 'e let read_reg reg state = let v = reg.read_from state.regstate in [(Value v,state)] diff --git a/src/rewrites.ml b/src/rewrites.ml index 99105a6d..074ad60f 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1884,7 +1884,12 @@ let rewrite_fix_val_specs (Defs defs) = TypSchm_aux (TypSchm_ts (tq, typ), Parse_ast.Unknown), val_specs end else begin let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in - typschm, Bindings.add id (tq, typ) val_specs + (* Add rreg effect to internal _reg_deref function (cf. bitfield.ml) *) + let vs = + if string_of_id id = "_reg_deref" then + add_eff_to_vs (mk_effect [BE_rreg]) (tq, typ) + else (tq, typ) in + typschm, Bindings.add id vs val_specs end in (val_specs, defs @ [DEF_spec (VS_aux (VS_val_spec (typschm, id, ext_opt, is_cast), a))]) |