Skip to content

Commit cefb4e8

Browse files
relokinmurzinv
authored and
artkhyzha
committed
[all] Turn labels into regular symbols
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com> Co-authored-by: Vladimir Murzin <vladimir.murzin@arm.com>
1 parent 9da8105 commit cefb4e8

40 files changed

+335
-238
lines changed

‎herd/AArch64Arch_herd.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -123,7 +123,7 @@ module Make (C:Arch_herd.Config)(V:Value.AArch64) =
123123
| V.Val Instruction i -> is_cmodx_restricted_instruction i
124124
| V.Val
125125
(Symbolic _|Concrete _|ConcreteVector _|ConcreteRecord _|
126-
Label _|Tag _|PteVal _|AddrReg _|Frozen _)
126+
Tag _|PteVal _|AddrReg _|Frozen _)
127127
| V.Var _ -> false
128128

129129
let ifetch_value_sets = [("Restricted-CMODX",is_cmodx_restricted_value)]

‎herd/AArch64Sem.ml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3438,7 +3438,7 @@ Arguments:
34383438
(*********************)
34393439

34403440
let make_label_value proc lbl_str =
3441-
A.V.cstToV (Constant.Label (proc, lbl_str))
3441+
A.V.cstToV (Constant.mk_sym_virtual_label proc lbl_str)
34423442

34433443
let read_loc_instr a ii =
34443444
M.read_loc Port.No (mk_fetch Annot.N) a ii
@@ -3450,7 +3450,7 @@ Arguments:
34503450
let v2tgt =
34513451
let open Constant in
34523452
function
3453-
| M.A.V.Val(Label (_, lbl)) -> Some (B.Lbl lbl)
3453+
| M.A.V.Val (Symbolic (Virtual {name=Symbol.Label (_, lbl); _})) -> Some (B.Lbl lbl)
34543454
| M.A.V.Val (Concrete i) -> Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
34553455
| _ -> None
34563456

@@ -3628,7 +3628,7 @@ Arguments:
36283628
>>= do_indirect_jump test [] i ii
36293629

36303630
| I_ERET ->
3631-
let eret_to_addr v =
3631+
let eret_to_addr v =
36323632
match v2tgt v with
36333633
| Some tgt -> B.faultRetT tgt
36343634
| _ ->

‎herd/ARMSem.ml‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -52,9 +52,12 @@ module
5252
let v2tgt =
5353
let open Constant in
5454
function
55-
| M.A.V.Val(Label (_, lbl)) -> Some (B.Lbl lbl)
56-
| M.A.V.Val (Concrete i) -> Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
57-
| _ -> None
55+
| M.A.V.Val (Symbolic (Virtual ({name=Symbol.Label (_,lbl); _}))) ->
56+
Some (B.Lbl lbl)
57+
| M.A.V.Val (Concrete i) ->
58+
Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
59+
| _ ->
60+
None
5861

5962

6063
(********************)

‎herd/ASLSem.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -400,7 +400,7 @@ module Make (Conf : Config) = struct
400400

401401
let binop_mod v1 v2 =
402402
match (v1, v2) with
403-
| ( (V.Val Constant.(Symbolic _ | Label _) | V.Var _),
403+
| ( (V.Val Constant.(Symbolic _) | V.Var _),
404404
V.Val (Constant.Concrete (ASLScalar.S_Int z)) )
405405
when is_valid_trailing_bits z ->
406406
return V.zero

‎herd/MIPSSem.ml‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -100,9 +100,12 @@ module
100100
let v2tgt =
101101
let open Constant in
102102
function
103-
| M.A.V.Val(Label (_, lbl)) -> Some (B.Lbl lbl)
104-
| M.A.V.Val (Concrete i) -> Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
105-
| _ -> None
103+
| M.A.V.Val(Symbolic (Virtual ({name=Symbol.Label (_,lbl); _}))) ->
104+
Some (B.Lbl lbl)
105+
| M.A.V.Val (Concrete i) ->
106+
Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
107+
| _ ->
108+
None
106109

107110
let do_indirect_jump test bds i v =
108111
match v2tgt v with

‎herd/X86_64Sem.ml‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -284,9 +284,12 @@ module
284284
let v2tgt =
285285
let open Constant in
286286
function
287-
| M.A.V.Val(Label (_, lbl)) -> Some (B.Lbl lbl)
288-
| M.A.V.Val (Concrete i) -> Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
289-
| _ -> None
287+
| M.A.V.Val (Symbolic (Virtual ({name=Symbol.Label (_,lbl); _}))) ->
288+
Some (B.Lbl lbl)
289+
| M.A.V.Val (Concrete i) ->
290+
Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
291+
| _ ->
292+
None
290293

291294
let do_indirect_jump test bds i v =
292295
match v2tgt v with

‎herd/archExtra_herd.ml‎

Lines changed: 16 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -414,8 +414,10 @@ module Make(C:Config) (I:I) : S with module I = I
414414
let get_symbol_name loc =
415415
let open Constant in
416416
match global loc with
417-
| Some (I.V.Val (Symbolic (Physical (name,_)|Virtual {name;_})))
417+
| Some (I.V.Val (Symbolic (Physical (name,_))))
418418
-> Some name
419+
| Some (I.V.Val (Symbolic (Virtual {name;_})))
420+
-> Some (Symbol.pp name)
419421
| _ -> None
420422

421423
let of_symbolic_data s =
@@ -486,8 +488,10 @@ module Make(C:Config) (I:I) : S with module I = I
486488
(* Compare id in fault and other id, at least one id must be allowed in fault *)
487489
let same_sym_fault sym1 sym2 = match sym1,sym2 with
488490
(* Both ids allowed in fault, compare *)
489-
|(Virtual {name=s1;_},Virtual {name=s2;_})
490-
|(System (PTE,s1),System (PTE,s2))
491+
| (Virtual {name=s1;_},Virtual {name=s2;_})
492+
-> Symbol.compare s1 s2 = 0
493+
| (System (PTE,s1),System (PTE,s2))
494+
(* | (System (TAG,s1),System (TAG,s2)) *)
491495
-> Misc.string_eq s1 s2
492496
(* One id allowed, the other on forbidden, does not match *)
493497
| (Virtual _,(System ((PTE|TLB|PTE2),_)|Physical _|TagAddr _))
@@ -508,11 +512,6 @@ module Make(C:Config) (I:I) : S with module I = I
508512
let same_id_fault v1 v2 = match v1,v2 with
509513
| I.V.Val (Symbolic sym1), I.V.Val (Symbolic sym2)
510514
-> same_sym_fault sym1 sym2
511-
| I.V.Val (Constant.Label (_, l1)),I.V.Val (Constant.Label (_, l2))
512-
-> Misc.string_eq l1 l2
513-
| I.V.Val (Symbolic _), I.V.Val (Constant.Label (_, _))
514-
| I.V.Val (Constant.Label (_, _)), I.V.Val (Symbolic _)
515-
-> false
516515
| _,_
517516
->
518517
Warn.fatal
@@ -762,7 +761,7 @@ module Make(C:Config) (I:I) : S with module I = I
762761
let tag = None in
763762
let cap = 0L in
764763
let sym_data =
765-
{ Constant.name=s ;
764+
{ Constant.name=Constant.Symbol.Data s ;
766765
tag=tag ;
767766
cap=cap ;
768767
offset=i*nbytes;
@@ -835,12 +834,16 @@ module Make(C:Config) (I:I) : S with module I = I
835834
| Location_global
836835
(I.V.Val
837836
(Concrete _|ConcreteVector _|ConcreteRecord _
838-
|Label _|Instruction _|Frozen _
837+
|Instruction _|Frozen _
839838
|Tag _|PteVal _|AddrReg _))
840839
->
841840
Warn.user_error
842841
"Very strange location (look_address) %s\n"
843842
(pp_location loc)
843+
| Location_global (I.V.Val (Symbolic (Virtual {name=n;_}))) when Symbol.is_label n ->
844+
Warn.user_error
845+
"No default value defined for location %s\n"
846+
(pp_location loc)
844847
| Location_global (I.V.Val (Symbolic (Virtual _|Physical _)))
845848
| Location_reg _ -> reg_default_value
846849

@@ -870,15 +873,15 @@ module Make(C:Config) (I:I) : S with module I = I
870873

871874
let look_size_location env loc =
872875
match symbolic_data loc with
873-
| Some {Constant.name=s;_} -> look_size env s
876+
| Some {Constant.name=s;_} -> look_size env (Constant.Symbol.pp s)
874877
| _ -> assert false
875878

876879
let build_size_env bds =
877880
List.fold_left
878881
(fun m (loc,(t,_)) ->
879882
match symbolic_data loc with
880883
| Some sym ->
881-
StringMap.add sym.Constant.name (mem_access_size_of_t t) m
884+
StringMap.add (Constant.Symbol.pp sym.Constant.name) (mem_access_size_of_t t) m
882885
| _ -> m)
883886
size_env_empty bds
884887

@@ -1081,7 +1084,7 @@ module Make(C:Config) (I:I) : S with module I = I
10811084
| Location_global
10821085
(I.V.Val (Symbolic (Virtual {name=s; offset=_;_})) as a)
10831086
->
1084-
let sz = look_size senv s in
1087+
let sz = look_size senv (Constant.Symbol.pp s) in
10851088
let eas = byte_eas sz a in
10861089
let vs = List.map (get_of_val st) eas in
10871090
let v = recompose vs in

‎herd/eventsMonad.ml‎

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -886,7 +886,8 @@ Monad type:
886886
let eiid,(act,_) = g lbl eiid in
887887
let f (r,cs,es) =
888888
let cs =
889-
VC.Assign (v,VC.Atom (V.Val (Constant.Label (p,lbl))))::cs in
889+
let symb = Constant.mk_sym_virtual_label p lbl in
890+
VC.Assign (v,VC.Atom (V.Val symb))::cs in
890891
r,cs,es in
891892
eiid,(Evt.map f act,None) in
892893
(* Rec *)
@@ -1403,8 +1404,9 @@ Monad type:
14031404
| _ -> false
14041405

14051406
let is_instrloc a =
1407+
let open Constant in
14061408
match a with
1407-
| V.Val (Constant.Label _) -> true
1409+
| V.Val (Symbolic (Virtual {name=n; _})) -> Symbol.is_label n
14081410
| _ -> false
14091411

14101412
(*
@@ -1461,7 +1463,7 @@ Monad type:
14611463
E.action =
14621464
E.Act.mk_init_write
14631465
(A.of_symbolic_data
1464-
{default_symbolic_data with name=Misc.add_ctag s})
1466+
{default_symbolic_data with name=Symbol.Data (Misc.add_ctag s)})
14651467
(def_size v) v; }
14661468

14671469
let debug_env env =
@@ -1505,6 +1507,7 @@ Monad type:
15051507
| A.Location_global
15061508
(V.Val
15071509
(Symbolic (Virtual {name=s; tag=None; offset=o;_}))) ->
1510+
let s = Symbol.pp s in
15081511
(phy_loc s o,v)::env,
15091512
(StringSet.add s virt,pte)
15101513
| A.Location_global (V.Val (Symbolic (System (PTE,s)))) ->
@@ -1580,7 +1583,7 @@ Monad type:
15801583
if morello then
15811584
let eiid,em =
15821585
morello_init_tag
1583-
s (V.op1 Op.CapaGetTag v) eiid in
1586+
(Constant.Symbol.pp s) (V.op1 Op.CapaGetTag v) eiid in
15841587
eiid,(em::[ew])
15851588
else eiid,[ew] in
15861589
(eiid,ews@es)
@@ -1615,9 +1618,9 @@ Monad type:
16151618
(Symbolic
16161619
(Virtual
16171620
{name=s;offset=_;_})) as a)
1618-
when not (Misc.check_atag s) ->
1621+
when not (Misc.check_atag (Symbol.pp s)) ->
16191622
(* Suffix encoding of tag addresses, sufficient for now *)
1620-
let sz = A.look_size size_env s in
1623+
let sz = A.look_size size_env (Symbol.pp s) in
16211624
let ds = AM.explode sz v
16221625
and eas = AM.byte_eas sz a in
16231626
let eiid,ews =
@@ -1634,7 +1637,7 @@ Monad type:
16341637
if morello then
16351638
let eiid,em =
16361639
morello_init_tag
1637-
s (V.op1 Op.CapaGetTag v)
1640+
(Symbol.pp s) (V.op1 Op.CapaGetTag v)
16381641
eiid in
16391642
eiid,em::ews
16401643
else eiid,ews in

‎herd/machAction.ml‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -104,8 +104,6 @@ end = struct
104104
if kvm then Access.PTE
105105
else Warn.fatal "PTE %s while -variant kvm is not active"
106106
(A.pp_location loc)
107-
| A.Location_global (V.Val (Label(_,_)))
108-
-> Access.VIR
109107
| A.Location_global v ->
110108
Warn.fatal
111109
"access_of_location_std on non-standard symbol '%s'"
@@ -611,7 +609,7 @@ end = struct
611609
| Some
612610
(A.V.Val
613611
(ConcreteVector _|Concrete _|Symbolic _|ConcreteRecord _
614-
|Label (_, _)|Tag _|Instruction _|AddrReg _
612+
|Tag _|Instruction _|AddrReg _
615613
|Frozen _))
616614
| None
617615
-> None

0 commit comments

Comments
 (0)