diff options
| -rw-r--r-- | src/gen_lib/state.lem | 12 | ||||
| -rw-r--r-- | src/pretty_print.ml | 40 |
2 files changed, 31 insertions, 21 deletions
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index eeff4717..7777cf5e 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -74,8 +74,8 @@ let write_memory addr l (V bits _ _) s = let bytes = byte_chunks l bits in (Left (), <| s with memstate = foldl write_memstate s.memstate (zip addrs bytes) |>) -val read_reg_range : forall 'e. register -> (integer * integer) (*(nat * nat)*) -> M state 'e (vector bit) -let read_reg_range reg (i,j) s = +val read_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> M state 'e (vector bit) +let read_reg_range reg i j s = let v = slice (read_regstate s reg) i j in (Left v,s) @@ -84,8 +84,8 @@ let read_reg_bit reg i s = let v = access (read_regstate s reg) i in (Left v,s) -val write_reg_range : forall 'e. register -> (integer * integer) (*(nat * nat)*) -> vector bit -> M state 'e unit -let write_reg_range (reg : register) (i,j) (v : vector bit) s = +val write_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> vector bit -> M state 'e unit +let write_reg_range reg i j v s = let v' = update (read_regstate s reg) i j v in let s' = write_regstate s reg v' in (Left (),s') @@ -148,10 +148,10 @@ let rec foreachM_dec (i,stop,by) vars body = else return ((),vars) val read_reg_field : forall 'e. register -> register_field -> M state 'e (vector bit) -let read_reg_field reg rfield = read_reg_range reg (field_indices rfield) +let read_reg_field reg rfield = uncurry (read_reg_range reg) (field_indices rfield) val write_reg_field : forall 'e. register -> register_field -> vector bit -> M state 'e unit -let write_reg_field reg rfield = write_reg_range reg (field_indices rfield) +let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield) val read_reg_field_bit : forall 'e. register -> register_field_bit -> M state 'e bit let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit) diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 7e2e87b0..1e8f185c 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -2082,25 +2082,35 @@ let doc_exp_lem, doc_let_lem = if aexp_needed then parens (align epp) else epp ) ) - | E_vector_access(v,e) -> - let epp = separate space [string "access";exp v;exp e] in + | E_vector_access (v,e) -> + let (Base (_,_,_,_,eff,_)) = annot in + let epp = + if has_rreg_effect eff then + separate space [string "read_reg_bit";exp v;exp e] + else + separate space [string "access";exp v;exp e] in if aexp_needed then parens (align epp) else epp - | E_vector_subrange(v,e1,e2) -> - let epp = align (string "slice" ^^ space ^^ exp v ^//^ exp e1 ^//^ exp e2) in + | E_vector_subrange (v,e1,e2) -> + let (Base (_,_,_,_,eff,_)) = annot in + let epp = + if has_rreg_effect eff then + align (string "read_reg_range" ^^ space ^^ exp v ^//^ exp e1 ^//^ exp e2) + else + align (string "slice" ^^ space ^^ exp v ^//^ exp e1 ^//^ exp e2) in if aexp_needed then parens (align epp) else epp | E_field((E_aux(_,(_,fannot)) as fexp),id) -> let (Base ((_,{t = t}),_,_,_,_,_)) = fannot in - (match t with - | Tabbrev({t = Tid regtyp},{t=Tapp("register",_)}) -> - let field_f = match annot with - | Base((_,{t = Tid "bit"}),_,_,_,_,_) - | Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) -> - string "read_reg_field_bit" - | _ -> string "read_reg_field" in - let epp = field_f ^^ space ^^ (exp fexp) ^^ space ^^ - string (regtyp ^ "_") ^^ doc_id_lem id in - if aexp_needed then parens (align epp) else epp - | _ -> exp fexp ^^ dot ^^ doc_id_lem id) + (match t with + | Tabbrev({t = Tid regtyp},{t=Tapp("register",_)}) -> + let field_f = match annot with + | Base((_,{t = Tid "bit"}),_,_,_,_,_) + | Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) -> + string "read_reg_field_bit" + | _ -> string "read_reg_field" in + let epp = field_f ^^ space ^^ (exp fexp) ^^ space ^^ + string (regtyp ^ "_") ^^ doc_id_lem id in + if aexp_needed then parens (align epp) else epp + | _ -> exp fexp ^^ dot ^^ doc_id_lem id) | E_block [] -> string "()" | E_block exps -> failwith "Blocks should have been removed till now." | E_nondet exps -> failwith "Nondet blocks not supported." |