Skip to content

[all] Turn labels into symbols #1577

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
artkhyzha merged 1 commit into from
Dec 5, 2025
Merged

[all] Turn labels into symbols #1577

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion herd/AArch64Arch_herd.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ module Make (C:Arch_herd.Config)(V:Value.AArch64) =
| V.Val Instruction i -> is_cmodx_restricted_instruction i
| V.Val
(Symbolic _|Concrete _|ConcreteVector _|ConcreteRecord _|
Label _|Tag _|PteVal _|AddrReg _|Frozen _)
Tag _|PteVal _|AddrReg _|Frozen _)
| V.Var _ -> false

let ifetch_value_sets = [("Restricted-CMODX",is_cmodx_restricted_value)]
Expand Down
6 changes: 3 additions & 3 deletions herd/AArch64Sem.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3438,7 +3438,7 @@ Arguments:
(*********************)

let make_label_value proc lbl_str =
A.V.cstToV (Constant.Label (proc, lbl_str))
A.V.cstToV (Constant.mk_sym_virtual_label proc lbl_str)

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

Expand Down Expand Up @@ -3628,7 +3628,7 @@ Arguments:
>>= do_indirect_jump test [] i ii

| I_ERET ->
let eret_to_addr v =
let eret_to_addr v =
match v2tgt v with
| Some tgt -> B.faultRetT tgt
| _ ->
Expand Down
9 changes: 6 additions & 3 deletions herd/ARMSem.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,9 +52,12 @@ module
let v2tgt =
let open Constant in
function
| M.A.V.Val(Label (_, lbl)) -> Some (B.Lbl lbl)
| M.A.V.Val (Concrete i) -> Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
| _ -> None
| M.A.V.Val (Symbolic (Virtual ({name=Symbol.Label (_,lbl); _}))) ->
Some (B.Lbl lbl)
| M.A.V.Val (Concrete i) ->
Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
| _ ->
None


(********************)
Expand Down
2 changes: 1 addition & 1 deletion herd/ASLSem.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -400,7 +400,7 @@ module Make (Conf : Config) = struct

let binop_mod v1 v2 =
match (v1, v2) with
| ( (V.Val Constant.(Symbolic _ | Label _) | V.Var _),
| ( (V.Val Constant.(Symbolic _) | V.Var _),
V.Val (Constant.Concrete (ASLScalar.S_Int z)) )
when is_valid_trailing_bits z ->
return V.zero
Expand Down
9 changes: 6 additions & 3 deletions herd/MIPSSem.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,9 +100,12 @@ module
let v2tgt =
let open Constant in
function
| M.A.V.Val(Label (_, lbl)) -> Some (B.Lbl lbl)
| M.A.V.Val (Concrete i) -> Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
| _ -> None
| M.A.V.Val(Symbolic (Virtual ({name=Symbol.Label (_,lbl); _}))) ->
Some (B.Lbl lbl)
| M.A.V.Val (Concrete i) ->
Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
| _ ->
None

let do_indirect_jump test bds i v =
match v2tgt v with
Expand Down
9 changes: 6 additions & 3 deletions herd/X86_64Sem.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -284,9 +284,12 @@ module
let v2tgt =
let open Constant in
function
| M.A.V.Val(Label (_, lbl)) -> Some (B.Lbl lbl)
| M.A.V.Val (Concrete i) -> Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
| _ -> None
| M.A.V.Val (Symbolic (Virtual ({name=Symbol.Label (_,lbl); _}))) ->
Some (B.Lbl lbl)
| M.A.V.Val (Concrete i) ->
Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
| _ ->
None

let do_indirect_jump test bds i v =
match v2tgt v with
Expand Down
29 changes: 16 additions & 13 deletions herd/archExtra_herd.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -414,8 +414,10 @@ module Make(C:Config) (I:I) : S with module I = I
let get_symbol_name loc =
let open Constant in
match global loc with
| Some (I.V.Val (Symbolic (Physical (name,_)|Virtual {name;_})))
| Some (I.V.Val (Symbolic (Physical (name,_))))
-> Some name
| Some (I.V.Val (Symbolic (Virtual {name;_})))
-> Some (Symbol.pp name)
| _ -> None

let of_symbolic_data s =
Expand Down Expand Up @@ -486,8 +488,10 @@ module Make(C:Config) (I:I) : S with module I = I
(* Compare id in fault and other id, at least one id must be allowed in fault *)
let same_sym_fault sym1 sym2 = match sym1,sym2 with
(* Both ids allowed in fault, compare *)
|(Virtual {name=s1;_},Virtual {name=s2;_})
|(System (PTE,s1),System (PTE,s2))
| (Virtual {name=s1;_},Virtual {name=s2;_})
-> Symbol.compare s1 s2 = 0
| (System (PTE,s1),System (PTE,s2))
(* | (System (TAG,s1),System (TAG,s2)) *)
-> Misc.string_eq s1 s2
(* One id allowed, the other on forbidden, does not match *)
| (Virtual _,(System ((PTE|TLB|PTE2),_)|Physical _|TagAddr _))
Expand All @@ -508,11 +512,6 @@ module Make(C:Config) (I:I) : S with module I = I
let same_id_fault v1 v2 = match v1,v2 with
| I.V.Val (Symbolic sym1), I.V.Val (Symbolic sym2)
-> same_sym_fault sym1 sym2
| I.V.Val (Constant.Label (_, l1)),I.V.Val (Constant.Label (_, l2))
-> Misc.string_eq l1 l2
| I.V.Val (Symbolic _), I.V.Val (Constant.Label (_, _))
| I.V.Val (Constant.Label (_, _)), I.V.Val (Symbolic _)
-> false
| _,_
->
Warn.fatal
Expand Down Expand Up @@ -762,7 +761,7 @@ module Make(C:Config) (I:I) : S with module I = I
let tag = None in
let cap = 0L in
let sym_data =
{ Constant.name=s ;
{ Constant.name=Constant.Symbol.Data s ;
tag=tag ;
cap=cap ;
offset=i*nbytes;
Expand Down Expand Up @@ -835,12 +834,16 @@ module Make(C:Config) (I:I) : S with module I = I
| Location_global
(I.V.Val
(Concrete _|ConcreteVector _|ConcreteRecord _
|Label _|Instruction _|Frozen _
|Instruction _|Frozen _
|Tag _|PteVal _|AddrReg _))
->
Warn.user_error
"Very strange location (look_address) %s\n"
(pp_location loc)
| Location_global (I.V.Val (Symbolic (Virtual {name=n;_}))) when Symbol.is_label n ->
Warn.user_error
"No default value defined for location %s\n"
(pp_location loc)
| Location_global (I.V.Val (Symbolic (Virtual _|Physical _)))
| Location_reg _ -> reg_default_value

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

let look_size_location env loc =
match symbolic_data loc with
| Some {Constant.name=s;_} -> look_size env s
| Some {Constant.name=s;_} -> look_size env (Constant.Symbol.pp s)
| _ -> assert false

let build_size_env bds =
List.fold_left
(fun m (loc,(t,_)) ->
match symbolic_data loc with
| Some sym ->
StringMap.add sym.Constant.name (mem_access_size_of_t t) m
StringMap.add (Constant.Symbol.pp sym.Constant.name) (mem_access_size_of_t t) m
| _ -> m)
size_env_empty bds

Expand Down Expand Up @@ -1081,7 +1084,7 @@ module Make(C:Config) (I:I) : S with module I = I
| Location_global
(I.V.Val (Symbolic (Virtual {name=s; offset=_;_})) as a)
->
let sz = look_size senv s in
let sz = look_size senv (Constant.Symbol.pp s) in
let eas = byte_eas sz a in
let vs = List.map (get_of_val st) eas in
let v = recompose vs in
Expand Down
17 changes: 10 additions & 7 deletions herd/eventsMonad.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -886,7 +886,8 @@ Monad type:
let eiid,(act,_) = g lbl eiid in
let f (r,cs,es) =
let cs =
VC.Assign (v,VC.Atom (V.Val (Constant.Label (p,lbl))))::cs in
let symb = Constant.mk_sym_virtual_label p lbl in
VC.Assign (v,VC.Atom (V.Val symb))::cs in
r,cs,es in
eiid,(Evt.map f act,None) in
(* Rec *)
Expand Down Expand Up @@ -1403,8 +1404,9 @@ Monad type:
| _ -> false

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

(*
Expand Down Expand Up @@ -1461,7 +1463,7 @@ Monad type:
E.action =
E.Act.mk_init_write
(A.of_symbolic_data
{default_symbolic_data with name=Misc.add_ctag s})
{default_symbolic_data with name=Symbol.Data (Misc.add_ctag s)})
(def_size v) v; }

let debug_env env =
Expand Down Expand Up @@ -1505,6 +1507,7 @@ Monad type:
| A.Location_global
(V.Val
(Symbolic (Virtual {name=s; tag=None; offset=o;_}))) ->
let s = Symbol.pp s in
(phy_loc s o,v)::env,
(StringSet.add s virt,pte)
| A.Location_global (V.Val (Symbolic (System (PTE,s)))) ->
Expand Down Expand Up @@ -1580,7 +1583,7 @@ Monad type:
if morello then
let eiid,em =
morello_init_tag
s (V.op1 Op.CapaGetTag v) eiid in
(Constant.Symbol.pp s) (V.op1 Op.CapaGetTag v) eiid in
eiid,(em::[ew])
else eiid,[ew] in
(eiid,ews@es)
Expand Down Expand Up @@ -1615,9 +1618,9 @@ Monad type:
(Symbolic
(Virtual
{name=s;offset=_;_})) as a)
when not (Misc.check_atag s) ->
when not (Misc.check_atag (Symbol.pp s)) ->
(* Suffix encoding of tag addresses, sufficient for now *)
let sz = A.look_size size_env s in
let sz = A.look_size size_env (Symbol.pp s) in
let ds = AM.explode sz v
and eas = AM.byte_eas sz a in
let eiid,ews =
Expand All @@ -1634,7 +1637,7 @@ Monad type:
if morello then
let eiid,em =
morello_init_tag
s (V.op1 Op.CapaGetTag v)
(Symbol.pp s) (V.op1 Op.CapaGetTag v)
eiid in
eiid,em::ews
else eiid,ews in
Expand Down
4 changes: 1 addition & 3 deletions herd/machAction.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,8 +104,6 @@ end = struct
if kvm then Access.PTE
else Warn.fatal "PTE %s while -variant kvm is not active"
(A.pp_location loc)
| A.Location_global (V.Val (Label(_,_)))
-> Access.VIR
| A.Location_global v ->
Warn.fatal
"access_of_location_std on non-standard symbol '%s'"
Expand Down Expand Up @@ -611,7 +609,7 @@ end = struct
| Some
(A.V.Val
(ConcreteVector _|Concrete _|Symbolic _|ConcreteRecord _
|Label (_, _)|Tag _|Instruction _|AddrReg _
|Tag _|Instruction _|AddrReg _
|Frozen _))
| None
-> None
Expand Down
Loading