[gen] add @before and @after predicates for relaxations in diy7

[ShaleXIONG]

Add diy7-only predicate syntax for relax inputs:

• @before(...)
• @after(...)

The parser entry points are split so predicate syntax is accepted only by diy7. The shared main/diyone7, diycross7, and cumul parsers reject predicate syntax.

During relax expansion, invalid predicate placement is filtered before search:

• @before(...) is only valid at the start of a relaxation sequence
• @after(...) is only valid at the end of a relaxation sequence
• predicates in the middle of a concrete composition are discarded

During diy7 cycle search, boundary predicates are checked against neighbouring concrete edges. Once checked, predicates are stripped before passing candidate cycles to the normal test generator.

Added tests for:

• diy7 parser acceptance of @before(...) and @after(...), while other parsers reject of predicate syntax
• filtering invalid predicate placement to []
• In diy7 cycle generation, the predicates @beforeand @after merge as expected

Example

diy7 -arch AArch64 -cycleonly true -size 4 -relax '[@before(Po) PodRW Rfe @after(Po)]' -safe Po

This constrains the generated boundary edges to match the predicates. Po will match @before(Po) and after(Po) during the searching.

Generator produced 2 tests
Relaxations tested: {[@before(PosRR),PodRW,Rfe,@after(PosRR)]} {[@before(PodRR),PodRW,Rfe,@after(PodRR)]}
LB000: PosRR PodRW Rfe PosRR PodRW Rfe
LB001: PodRR PodRW Rfe PodRR PodRW Rfe

Another example contains composite relax:

diy7 -arch AArch64 -cycleonly true -size 4 -relax '[PodRW Rfe @after([PodRW Rfe])]'

In this case, the only relaxation will be match with themselves, i.e., the leading PodRW Rfe matches the trailing @after([PodRW Rfe]).

Generator produced 3 tests
Relaxations tested: {[PodRW,Rfe,@after(PodRW),@after(Rfe)]}
LB000: PodRW Rfe PodRW Rfe
3.LB000: PodRW Rfe PodRW Rfe PodRW Rfe
4.LB000: PodRW Rfe PodRW Rfe PodRW Rfe PodRW Rfe

[fsestini]

Thanks @ShaleXIONG . I had a first look at the PR. I'm still trying to digest it, so most of the comments I left are questions/clarifications. In particular, I think the changes in alt.ml are a bit hard to review as they are, and there should be things we can do to make the diff more readable. See the comment on that file for more details.

[fsestini]

This file is difficult to review in its current form because the predicate-related change is mixed with quite a few changes that seem unrelated at first sight.

For example:

• Several existing local names are renamed even when their role has not changed, for example the call_rec_base parameter f0 is renamed to test_generator.
• Many comments explaining almost every individual line, to an excessive degree in my view.
• Some existing helpers seem to have been renamed and rewritten rather than minimally adapted. For example, the old c_minprocs_es, c_minprocs_suff, c_minint_es, and c_minint helpers are replaced by procedure_count, max_edges_in_procedure, etc. I completely see the value in refreshing the names and implementation of some of these functions, however I don't think this PR is the right time for that.
• Some of the changes look potentially semantic, not merely cosmetic. For example, inside call_rec_base, the old code used let n = n - sz r, whereas the new code uses let n = n - 1. It's not immediately clear to me whether this is a simple refactor or an important change in the logic.

Could you please rework the changes in this file so that the diff is as small and targeted as possible? In case some of these seemingly cosmetic changes are actually necessary for the functionality of the PR, could you please elaborate on those.

Concretely, I would prefer if we can keep these to a minimum:

• renaming of existing functions or parameters
• whitespace/indentation changes
• added/removed begin/end
• line-by-line comments unless there's some particular complex sequence that needs extra discussion

[ShaleXIONG]

Let me separate some semantics equivalent change from the history as I did this a while ago to .

To answer some of your questions immediately:
-c_minprocs_es,c_minprocs_suff, c_minint_es and c_minint are semantic equivalent change. As you suggested here, it is for better naming and also I try to rewrite with standard library function such as fold_left.

• n = n - sz r is a bug fix or clarification. The search algorithm will stop after certain size default 6. An input relax, including composite relax such as [PosWR Fre] counts as one. However, if the input only contain annotations such as A, it does not count. This is unnecessary behaviour and also there is no use case we explicitly do not want to count individual annotation A.

[fsestini]

That makes sense. I think these two are changes worth making, however I'd say they aren't very relevant to the predicate feature being introduced here. Their concerns are also different enough to warrant their own dedicated PR.

I would therefore suggest submitting these two changes (semantics-preserving refactoring and n = n - sz r bug fix) as two distinct PRs separate from the current one. Same treatment can be given to other changes in alt.ml that are not related to predicates.

[ShaleXIONG]

I have rewrite the history which should be much simpler now. Will open separate PRs later.

[fsestini]

I am not completely convinced adding this pred : edge_predicate option to the common edge type is the right abstraction, though admittedly I don't have a strong alternative to propose at the moment. I can see the implementation reason for this choice, since the field is used in alt.ml. However, from the perspective of someone reading the declaration of edge in edge.ml, I think this pred field might be slightly confusing.

First of all, it's not immediately clear what it means for an edge to have a predicate field set. What does that field indicate? How is an edge "with a predicate" different from one "without"?

Secondly, AFAIU these predicates are supposed to be a diy7-specific mechanism. However, here predicates are being added to the common edge type (used by all gen/ tools) as if they were an intrinsic property of edge in general. Indeed if we look at how the pred field is used in edge.ml, it is pretty much always set pred = None or ignored. I'm concerned that we might be leaking diy7-specific concepts into the common edge abstraction.

Curious if you have thought about using a different, diy7-specific predicate-aware relaxation type for this, instead of the common edge type? (That would mean the cycle search code would have to be adapted to operate on that representation instead.)

[ShaleXIONG]

For the question of meaning of predicate, there is no unifying meaning of predicates in general. We currently have before and after. We might add more based on need/requirements. They are ad-hoc extension of the expressibility and directly bind to code level for sure. I am trying to avoid introducing a full language here. Also I will prefer if something can be done without predicate.

For the changing of type edge, I do not have good solution neither tbh, as the diy7 searching algorithm is based on type edge. I made the minimum change to the code here. Alternative idea might be keep the predicate in the Ast level, however this mean we need to rework the entire alt.ml, i.e., searching algorithm to take an Ast as input rather than edge list list.

[fsestini]

directly bind to code level

Not sure I follow. Can you clarify what you mean by this?

Alternative idea might be keep the predicate in the Ast level, however this mean we need to rework the entire alt.ml, i.e., searching algorithm to take an Ast as input rather than edge list list.

That would be a slight improvement, but you'd still be tying the search algorithm to a concrete data structure, one that just happens to be different from edge list list. As you correctly noted, this dependence of the search algo on a specific concrete data type is precisely what makes it non-modular and harder to extend, something that has affected the choices taken in this PR. So perhaps we could instead focus on making alt.ml more modular.

Could you have a look and estimate how hard it would be to refactor alt.ml into a functor, so that the cycle search algorithm is expressed parametrically w.r.t. an abstract type and abstract operations that are passed as a parameter? Something along the lines of how this normalisation algo operates on abstract types passed as functor parameters.

[ShaleXIONG]

Yes you are right the searching algorithm will still largely base on the concrete type of edge (If assume one particular architecture backend). Yet we can do something local to alt.ml such as the entire input will be a Ast.t, then internal we can have some data type such as type edge_pred = Edge of edge | Predicate of pred*edge. The current Alt is actually a functor, taking an argument C:Builder.S which corresponds to different architecture backend. The may interface is gen which take relax list aka equivalent edge list list as the inputs.

I will have a look of possible refactoring here further. Given how intertwine of all the module and functor in diy*, it will be a sizeable re-organisation of code. Yet I do not see any blocker and we possibly want to do in a separate PR.

[fsestini]

The current Alt is actually a functor, taking an argument C:Builder.S which corresponds to different architecture backend.

You're right. What I'm suggesting is to functorise the search algorithm part so that the cycle data structure is provided as a parameter. Perhaps this entails extending an existing functor.

I will have a look of possible refactoring here further. Given how intertwine of all the module and functor in diy*, it will be a sizeable re-organisation of code. Yet I do not see any blocker and we possibly want to do in a separate PR.

Thanks! Also, happy to discuss this further on a dedicated GH issue.

[fsestini]

Let's not use the builtin polymorphic equality please. Let's use dedicated equal predicates or similar.

[ShaleXIONG]

I have pipe through several equal_* function in different places so to remove this polymorphic equality check. Will keep this extra change in a separate commit in the history.

[fsestini]

I find Warn.user_error here a bit misleading. This ast is parsed with Parser.cumul, which grammar does not accept predicates. So if the user writes a predicate in the -cumul input, parsing should already fail before Ast.expand is reached. In other words, this fun _ -> Warn.user_error ... function should be unreachable under the current parser implementation, and it only exists only because Ast.expand requires it.

Could we use something that makes this aspect clearer, such as failwith/assert false/Warn.fatal, rather than Warn.user_error? A user_error here implicitly suggests that this is part of normal input validation and that this line could be reached under bad user input, however that is not the case.

[ShaleXIONG]

It is my mistake. I will change it to Warn.fatal

[fsestini]

Could you clarify what this does?

[ShaleXIONG]

It check: before predicates must form a leading prefix and after predicates must form a trailing suffix. I added comment above this function now.