Skip to content

Commit 80e1a62

Browse files
committed
fix: define code_instr in its own module
1 parent 3166759 commit 80e1a62

File tree

3 files changed

+24
-18
lines changed

3 files changed

+24
-18
lines changed

herd/archExtra_herd.ml

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -73,10 +73,13 @@ module type S = sig
7373
and ready to start, plus some items that describe
7474
the test, such as its name (cf. Test.mli) *)
7575

76-
type code_instr = { instr: instr; static_poi: int }
76+
77+
module CodeInstr : sig
78+
type t = { instr: instr; static_poi: int }
79+
end
7780

7881
(* Code memory is a mapping from labels to sequences of instructions, too far from actual machine, maybe *)
79-
type code = (int * code_instr) list
82+
type code = (int * CodeInstr.t) list
8083

8184
val convert_if_imm_branch : int -> int -> int Label.Map.t -> int Label.Map.t -> instr -> instr
8285

@@ -338,10 +341,12 @@ module Make(C:Config) (I:I) : S with module I = I
338341
(* Components of test structures *)
339342
(*********************************)
340343

341-
type code_instr = { instr: instr; static_poi: int }
344+
module CodeInstr = struct
345+
type t = { instr: instr; static_poi: int }
346+
end
342347

343348
(* Code memory is a mapping from globals locs, to instructions *)
344-
type code = (int * code_instr) list
349+
type code = (int * CodeInstr.t) list
345350

346351
(* This function is a default behaviour for all architectures.
347352
When variant -self is enabled, it fails trying to convert a branch

herd/loader.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ struct
9696
load_code proc (addr+A.size_of_ins ins) (static_poi+1) mem rets code in
9797
let new_ins =
9898
convert_lbl_to_offset proc addr mem ins in
99-
let code_ins = { A.instr = new_ins; A.static_poi; } in
99+
let code_ins = { A.CodeInstr.instr = new_ins; static_poi; } in
100100
let new_start = (addr, code_ins) :: start in
101101
let newer_rets = IntMap.add addr (proc,new_start) new_rets in
102102
new_start,newer_rets

herd/mem.ml

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -164,6 +164,7 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S =
164164
module VC = EM.VC
165165
module U = MemUtils.Make(S)
166166
module W = Warn.Make(C)
167+
module CodeInstr = A.CodeInstr
167168

168169
let dbg = C.debug.Debug_herd.mem
169170
let morello = C.variant Variant.Morello
@@ -297,14 +298,14 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S =
297298
| Some fh_code -> code@fh_code
298299
| None -> code in
299300
List.fold_left
300-
(fun locs (_, (i : A.code_instr)) ->
301+
(fun locs (_, (i : CodeInstr.t)) ->
301302
A.fold_addrs
302303
(fun x ->
303304
let loc = A.maybev_to_location x in
304305
match loc with
305306
| A.Location_global _ -> A.LocSet.add loc
306307
| _ -> fun locs -> locs)
307-
locs i.A.instr)
308+
locs i.CodeInstr.instr)
308309
locs code)
309310
locs
310311
test.Test_herd.start_points in
@@ -435,7 +436,7 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S =
435436
| Some lbl ->
436437
let symb = Constant.mk_sym_virtual_label proc lbl in
437438
let loc = A.Location_global (A.V.cstToV symb)
438-
and v = A.V.instructionToV i.A.instr in
439+
and v = A.V.instructionToV i.CodeInstr.instr in
439440
A.state_add env loc v)
440441
init_state lbls2i
441442
in
@@ -518,10 +519,10 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S =
518519
| e -> raise e in
519520

520521
(* Call instruction semantics proper *)
521-
let wrap re_exec fetch_proc proc (inst : A.code_instr) addr env m poi =
522+
let wrap re_exec fetch_proc proc (code_instr : CodeInstr.t) addr env m poi =
522523
profile "build semantics" @@ fun () ->
523-
let static_poi = inst.A.static_poi in
524-
let inst = inst.A.instr in
524+
let static_poi = code_instr.CodeInstr.static_poi in
525+
let inst = code_instr.CodeInstr.instr in
525526
let ii =
526527
{ A.program_order_index = poi;
527528
static_poi;
@@ -544,9 +545,9 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S =
544545
m ii in
545546

546547
let sem_instr = SM.build_semantics test in
547-
let rec add_next_instr re_exec fetch_proc proc env seen addr (i : A.code_instr) nexts =
548-
wrap re_exec fetch_proc proc i addr env sem_instr >>> fun branch ->
549-
let inst = i.A.instr in
548+
let rec add_next_instr re_exec fetch_proc proc env seen addr (code_instr : CodeInstr.t) nexts =
549+
wrap re_exec fetch_proc proc code_instr addr env sem_instr >>> fun branch ->
550+
let inst = code_instr.CodeInstr.instr in
550551
let { A.regs=env; lx_sz=szo; fh_code } = env in
551552
let env = A.kill_regs (A.killed inst) env
552553
and szo =
@@ -564,7 +565,7 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S =
564565
bds env
565566
| _ -> env in
566567
next_instr
567-
re_exec i fetch_proc proc { A.regs=env; lx_sz=szo; fh_code}
568+
re_exec code_instr fetch_proc proc { A.regs=env; lx_sz=szo; fh_code}
568569
seen addr nexts branch
569570

570571
and add_code re_exec fetch_proc proc env seen nexts = match nexts with
@@ -618,15 +619,15 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S =
618619
else (* execute again the same instruction *)
619620
add_next_instr true fetch_proc proc env seen addr inst nexts
620621

621-
and next_instr re_exec (inst : A.code_instr) fetch_proc proc env seen addr nexts b =
622+
and next_instr re_exec (code_instr : CodeInstr.t) fetch_proc proc env seen addr nexts b =
622623
match b with
623624
| S.B.Exit -> EM.unitcodeT true
624625
| S.B.Next _ ->
625626
add_code re_exec fetch_proc proc env seen nexts
626627
| S.B.Jump (tgt,_) ->
627628
add_tgt re_exec true proc env seen addr tgt
628629
| S.B.Fault (syscall,_) ->
629-
add_fault re_exec inst fetch_proc proc env seen addr syscall nexts
630+
add_fault re_exec code_instr fetch_proc proc env seen addr syscall nexts
630631
| S.B.FaultRet tgt ->
631632
add_tgt false true proc env seen addr tgt
632633
| S.B.CondJump (v,tgt) ->
@@ -2152,7 +2153,7 @@ let match_reg_events es =
21522153
Warn.user_error
21532154
"Instruction %s:%s cannot be overwritten"
21542155
(Label.pp lbl)
2155-
(A.dump_instruction i.A.instr)
2156+
(A.dump_instruction i.CodeInstr.instr)
21562157
with
21572158
| Not_found ->
21582159
Warn.user_error

0 commit comments

Comments
 (0)