Conversation
|
In principle, the intent is to merge #1518 soon, but since there is a bit of work to do on it, and since this specific commit has been creating a massive amount of conflicts, and since it is useful for another PR, I quite like @murzinv's idea to merge it quicker. @murzinv , @relokin -- what do you think, what do we need to merge this PR? My thinking is, this PR would likely affect:
|
artkhyzha
force-pushed
the
labels-are-now-symbols
branch
from
1e3da84 to
12e17be
Compare
artkhyzha
force-pushed
the
labels-are-now-symbols
branch
from
12e17be to
206f8e0
Compare
|
This PR, essentially, simply replaces treatment of labels as a special kind of constants with treatment of them as symbolic constants. (This is because we would like to extend the use of the syntax This is not meant to be a breaking change, but it conflicts with changes to constants, so to avoid repeated rebasing, there is an idea of merging this sooner rather than later. Please let me know if you have concerns. |
|
UPD. It occurred to me that the impact on Something to look into. |
diaolo01
left a comment
diaolo01
left a comment
There was a problem hiding this comment.
Hello @artkhyzha,
I had a look and the PR makes sense to me. I mostly focused on constant.ml and the parser changes, which seemed to be most significant.
| (*vector metadata - prim size (arg1) and total array size (arg2) *) | ||
| (*needed for is-non-mixed-symbol and global vectors *) | ||
|
|
||
| module Symbol = struct |
There was a problem hiding this comment.
I wonder if it would be worth moving this into a dedicated Symbol module, similar to how we treat PAC in the symbolic_data record.
There was a problem hiding this comment.
I do not have a strong opinion. Right now the code uses Constant.Symbol in various places. I don't think it's fundamental for it to be exposed through the interface of constants though. It could be hidden in side Constant, with wrapper functions made available.
Presently I do not clearly see what would be an improvement, so I'd opt for no action.
|
|
||
| let mk_sym_tagloc_zero s = do_mk_sym_tagloc s 0 | ||
|
|
||
| let mk_sym_morello p s t = |
There was a problem hiding this comment.
Same question as for mk_sym_tag.
There was a problem hiding this comment.
Same answer! Strictly speaking, this patch does not need this change, but when I picked up, it already moved some of these mk_* functions. This seems to be in line with constant.mli interface, so I am keeping the change as is unless there are strong opinions.
There was a problem hiding this comment.
UPD. It occurred to me that the impact on
litmus7could be tested too -- and there are regressions that show up when tests from the catalogue are run:File "catalogue/aarch64-ifetch/tests/DIC0-IDC0/MP.RF+cachesync+switch-ctrl.litmus" litmus cannot handle symbol '1:Lend' File "catalogue/aarch64-ifetch/tests/DIC0-IDC0/MP.RF+cachesync+switch-ctrlisb.litmus" litmus cannot handle symbol '1:Lend' File "catalogue/aarch64-ifetch/tests/DIC0-IDC0/MP.RF+dc-dsb-ic-dsb+addr.litmus" litmus cannot handle symbol '1:Lend' File "catalogue/aarch64-ifetch/tests/DIC0-IDC0/MP.RF+dc-dsb-ic-dsb+ctrlisb.br.litmus" litmus cannot handle symbol '1:Lend' File "catalogue/aarch64-ifetch/tests/DIC0-IDC0/miniJit01.litmus" litmus cannot handle symbol '1:L0' File "catalogue/aarch64-ifetch/tests/DIC0-IDC0/miniJit02.litmus" litmus cannot handle symbol '1:L0'Something to look into.
Here is (slightly tested) diff which makes problem go away
diff --git a/litmus/compile.ml b/litmus/compile.ml
index 60c986d9d..60d227cd3 100644
--- a/litmus/compile.ml
+++ b/litmus/compile.ml
@@ -210,7 +210,7 @@ module Generic
List.fold_left
(fun env (loc,(t,v)) -> match loc,v with
| _,Constant.Concrete _ -> env
- | A.Location_global _,Symbolic s ->
+ | A.Location_global _,Symbolic s when not (Constant.is_label v) ->
let a = A.Location_global (G.tr_symbol s) in
begin try
ignore (A.LocMap.find a env) ;
diff --git a/litmus/skel.ml b/litmus/skel.ml
index 91d83289e..088c30055 100644
--- a/litmus/skel.ml
+++ b/litmus/skel.ml
@@ -368,11 +368,8 @@ module Make
(* Right value, all cases *)
let rec dump_a_v = function
| Concrete i -> A.V.Scalar.pp Cfg.hexa i
- | Symbolic _ as v when is_label v ->
- Warn.user_error
- "Labels cannot be used as initial values of memory locations"
- | Symbolic (Virtual {name=s;tag=None; offset=0;_}) ->
- dump_a_addr (Symbol.pp s)
+ | Symbolic (Virtual {name=Symbol.Data s;tag=None; offset=0;_}) ->
+ dump_a_addr s
| ConcreteVector vs ->
let pps =
List.map
dea88e3 to
3e66500
Compare
|
This PR currently passes @maranget, would you have time to have a quick look at this PR? Essentially, the last concern I have is that this PR had conflicts with the changes that have been happening due to ASL+VMSA (I think). It would be helpful to know if any special care was needed in resolving the conflicts. |
artkhyzha
force-pushed
the
labels-are-now-symbols
branch
3 times, most recently
from
9c2ad51 to
0d90624
Compare
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com> Co-authored-by: Vladimir Murzin <vladimir.murzin@arm.com>
artkhyzha
force-pushed
the
labels-are-now-symbols
branch
from
0d90624 to
dd1bfd5
Compare
4 participants
This PR is a preparation for several strands of work, #1507 and #1518, which depend on treatment of labels as symbols rather than strings. With this PR, they would be treated more like virtual addresses, referred to as symbols like "x".
The use of labels in the syntax of litmus tests remains the same. No user-facing changes to the semantics of any feature of the tools are intended with this PR.