Does avenir support a program like my small modification to the hello example?

[jafingerhut]

I copied the directory synthesis/hello to a new synthesis/hello2 directory and modified the files target.p4 and fvs in my hello2 directory, as shown in the attached hello2.zip file.

I then ran the avenir command below, and was expecting that for a single table add to ipv4_fwd in abstract.p4, there would be 16 adds to my modified ipv4_fwd table in my target.p4 program, one for each of the 16 possible values of hdr.ivp4.ihl, but instead it seems to only create one such table entry, as shown below.

 ../avenir synth abstract.p4 target.p4 inserts.csv no_edits.csv fvs -b 1000 -e 10 -data inserts.csv -I1 includes -I2 includes -P4 -p --hint mask --cache-edits 1
solver child (pid 19370), exited with return code 0, exited
solver child (pid 19373), exited with return code 0, exited
Target operations:
ADD,ipv4_rewrite,hdr.ipv4.dstAddr ~ 0x0#32 ,0x0#48,0
ADD,ipv4_fwd,hdr.ipv4.dstAddr ~ 0x0#32 ,0x1#9,0

Is this a bug in avenir? A limitation based on some assumption in its design? Something else?

hello2.zip

[ericthewry]

Avenir doesn't support mixed match kinds. It assumes either everything is exact or everything is ternary (the default being that everything is ternary). IIRC wild-carded matches are not printed, so I think whats happening here is that the hdr.ipv4.ihl field is being wild-carded.

[jafingerhut]

Is there perhaps also an assumption that the target program tables will be ternary if the abstract program table is ternary? I ask because when I try a small modification to hello, as shown in the attached helllo4.zip program, where target.p4 tables are all exact, and abstract.p4 programs has an lpm table, avenir prints table_add commands for the target.p4 program that use masks, even though all of its tables are exact.

hello4.zip

[jafingerhut]

Perhaps you mean that avenir runs in one of these two modes:

(a) all table key field match_kind are treated as if they are ternary, regardless of what the match_kind is in the source code, for both abstract and target programs

(b) same as (a), but all treated as exact

Is that correct?

If so, what causes avenir to operate in mode (b)?

Is this behavior of ignoring the match_kind values in the source code a fundamental thing in the way Avenir works? Or just a simplifying assumption that made the development a bit faster, and Avenir could be generalized to obey the match_kind values in the P4 programs?