Fix expansion of signed ranges to masks #3212

vlstill · 2022-04-13T07:07:07Z

This fixes "#2800 Check whether the expansion of a range into ternary values is correct for signed numbers".

jafingerhut

I have reviewed the test programs and their -midend results output by the compiler, and they all look good to me. I have not attempted to review the C++ code changes.

jafingerhut · 2022-04-13T14:38:11Z

I am not familiar enough with the error output from the failing test to understand what it means, but perhaps that is output from the Gauntlet tests looking for non-equivalent programs output by the front or midend? If so, it might actually be a bug in the Gauntlet equivalence checker for this new feature, but again, I do not know enough about its output or implementation to be able to tell. @fruffy ?

mihaibudiu · 2022-04-13T23:17:48Z

midend/replaceSelectRange.cpp

@@ -21,7 +21,7 @@
 namespace P4 {

 std::vector<const IR::Mask *>
-DoReplaceSelectRange::rangeToMasks(const IR::Range *r) {
+DoReplaceSelectRange::rangeToMasks(const IR::Range *r, int keyIndex) {


I think it's actually nicer to return a list of vectors for the result.
one in the common case, two if the range contains 0.
the keyIndex and signedIndicesToReplace make the data flow much harder to understand.

I agree that signedIndicesToReplace does make the flow harder to understand. But this is mainly because it is indeed complex -- the indices are detected when range is expanded, but they are used in the corresponding select through which we backtrack later (making use of postorder). This needs to be done this way as at the time we encounter the select first, we don't know which values will contain ranges and when working with ranges we cannot replace a parent node (at least I don't think so, I could be wrong since I am a beginner to p4c). The only alternative to indices I see would be to remember the actual corresponding select expressions, but that in my opinion improves nothing and could lead to danger in case of some weird select with duplicated keys:

select (foo.a, foo.b, foo.a) { -5..5, 42, _ : ... _, 16, -32000 : ... }

In this (rather pathological) case, we need to insert the bitcast only to the first occurence of foo.a not to both instances of foo.a expression in select.

As for the vector-of-vectors. I don't think this is a good idea as returning a vector of vectors implies that there can be any number of vectors, including 0 and more than 2. Therefore I think that would be bad design of the function as the type would allow too many invalid possibilities. It could make sense to return pair (isSigned, vectors) and resolve the index one level up in the postorder of mask.

For now, I have just added a comment about the indices into the class.

mihaibudiu · 2022-04-13T23:19:02Z

midend/replaceSelectRange.cpp


-        range_size_remaining -= match_stride;
-        min += match_stride;
+        while (range_size_remaining > 0) {


Maybe this should become a separate function.

I have refactored the rangeToMasks function a bit since indeed it was quite long.

mihaibudiu · 2022-04-13T23:21:52Z

testdata/p4_16_samples/issue2800c.p4

+    state start {
+        packet.extract(hdr.h);
+        transition select(hdr.h.a, hdr.h.b) {
+            (0 .. 7, -5 .. 4): parse;


How about a test that has 2 ranges containing 0?

Sure, I have added one more test with two signed fields (not both of them are going over 0 since I realized I did not have any test for purely negative range. I think the "going over zero" case is covered sufficiently and this test mainly covers the missing "multiple fields are signed" case.

fruffy · 2022-04-13T23:24:18Z

@jafingerhut Let me check. Considering this is a new feature I am guessing the tool does not have support for it yet.

vlstill · 2022-04-14T07:31:32Z

@jafingerhut, @fruffy, looking at the output (not knowing what is is really :-D, but masing it on my knowledge of bit-vector SMT)

it seems to me this is having problems with frontend code (issue2800b-FrontEnd_0_P4V1::getV1ModelVersion.p4, issue2800b-FrontEnd_12_TypeInference.p4) which suggest the problem is with the input, not the code produced by midend
for hdr.h.a (model issue2800b) one of the inferred bounds is 65531 (0xfffc) which is unsigned reinterpretation of -5 which is the lower bound in the code. This suggests (together with use of bvule instead of bvsle (bit-vector unsigned/signed less then)) that the verifier is not working correctly with signed values
I think the condition is even more wrong (reformated & commented):

(let ((a!1 (ite  ; if
      (and (bvule #xfffb ((_ extract 31 16) extract_hdr))        ; 0xfffb <= extract_hdr[31:16]    (a)
           (= ((_ extract 31 19) extract_hdr) #b0000000000000)   ; and extract_hdr[31:19] == 0     (b)
           (bvule ((_ extract 18 16) extract_hdr) #b100)         ; and extract_hdr[18:16] <= 4     (c)
           (= ((_ extract 15 3) extract_hdr) #b0000000000000))   ; and extract_hdr[15:3] == 0      (d)
      #xffff ; then the result is 0xffff (that is -1, goign through 'parse' state)
      ((_ extract 31 16) extract_hdr)))) ; else it is the value extracted from the packet
    (ite extract_hdr_valid a!1 invalid))

obviously, the conditions (a) and (c) overlap (and (a) is wrong), but also (b) interacts weirdly with (a) in my opinion (if higher 13 bits are zero, then obviously the largest possible number would be 0x7 not 0xfffc) -> I would expect the zero check to be part of the other bound, but maybe this is just artefact of the mishandled constants again

vlstill · 2022-04-14T10:06:02Z

The condition is even clearer for the a test with only one field:

(let ((a!1 (ite ( ; if
        and (bvule #xfffb extract_hdr)                          ; 0xfffb <= extract_hdr   (a)
            (= ((_ extract 15 3) extract_hdr) #b0000000000000)  ; extract_hdr[15:3] == 0  (b)
            (bvule ((_ extract 2 0) extract_hdr) #b100)         ; extract_hdr[2:0] == 4   (c)
        ) ; end condition and
        #xffff ; <- then
        extract_hdr ; <- else
     )))
     (ite extract_hdr_valid a!1 invalid))

A correct and would have something like: (and (bvsle #xfffb extract_hdr) (bvsle extract_hdr 0x0004)).

fruffy · 2022-04-14T14:26:24Z

Thanks for looking into this? Yeah I believe it is a type conversion issue in the range matching. The validator uses its own type inference which may have flaws. I xfailed those couple programs until I have implemented the fix.

vlstill · 2022-04-14T16:57:26Z

@fruffy, thanks. So if @mbudiu-vmw is happy with my changes this can be merged.

mihaibudiu · 2022-04-15T20:43:38Z

midend/replaceSelectRange.cpp

@@ -115,12 +143,47 @@ DoReplaceSelectRange::cartesianAppend(const std::vector<IR::Vector<IR::Expressio
    return newVecs;
 }

+const IR::Node *DoReplaceSelectRange::preorder(IR::SelectExpression *e) {
+    BUG_CHECK(!inSelect, "A select nested in select: %1%", e);
+    inSelect = true;


In general you don't need such a boolean flag.
It can be replaced with findContext<IR::SelectExpression>() != nullptr, called from the child node.

This flag is there mostly to avoid introduction of more inconsistencies if AST is unexpected (or visitor is broken, which is probably significantly less likely). We could avoid it altogether but I believe a cheap assert is better then possibility on long debugging in future. If I replace it with findContext I don't think it would be that cheap.

The compiler code is not optimized for speed, but rather for correctness, readability, and maintainability. I think that findContext is more readable, and it is in only one place, so it is more maintainable.

mihaibudiu · 2022-04-15T20:49:08Z

midend/replaceSelectRange.h

+    // Collects select indices which will need to be replaced with bitcast of
+    // the original value to unsigned. This is needed if we encounter a range
+    // over a signed value at the given index.
+    std::set<int> signedIndicesToReplace;


why not a set of size_t or unsigned values?
I would change this comment to say "an index i is in this set if selectExpression->components[i] needs to be cast from int to bit". This is only needed if there is a label that has in the i-th position a range expression that contains 0 inside the range".

(Because old habits die hard.) Changed to size_t.

As for the comment, sure, except that we need to replace it any time the value is signed, not only when it crosses over zero. Masks are only defined for bit values in P4. I changed it.

mihaibudiu · 2022-04-15T20:49:20Z

These are minor changes requested.

vlstill added 4 commits April 11, 2022 15:02

Add compilation tests for signed ranges

8fa2514

ref p4lang#2800

Implement support for signed ranges

be08558

ref p4lang#2800

Add gtests for signed range rewriting size

34a3ffb

ref p4lang#2800

Add results for signed range tests

eff90ee

ref p4lang#2800

jafingerhut approved these changes Apr 13, 2022

View reviewed changes

mihaibudiu requested changes Apr 13, 2022

View reviewed changes

vlstill added 2 commits April 14, 2022 08:58

Add one more test for signed ranges

5681bfc

Remove extraneous debug prints from signed range gtests

80f68b9

vlstill added 2 commits April 14, 2022 10:45

Refactor select range replacement a bit

9444809

Add more gtests for signed ranges

a2c8f65

mihaibudiu requested changes Apr 15, 2022

View reviewed changes

vlstill added 3 commits April 19, 2022 10:22

Use size_t for indices

1a9a2d9

Update a comment

a62a610

Avoid the inSelect flag

aad48f4

mihaibudiu approved these changes Apr 20, 2022

View reviewed changes

mihaibudiu merged commit e1f0153 into p4lang:main Apr 20, 2022

vlstill mentioned this pull request Apr 25, 2022

Check whether the expansion of a range into ternary values is correct for signed numbers #2800

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix expansion of signed ranges to masks #3212

Fix expansion of signed ranges to masks #3212

vlstill commented Apr 13, 2022

jafingerhut left a comment

jafingerhut commented Apr 13, 2022

mihaibudiu Apr 13, 2022

vlstill Apr 14, 2022

mihaibudiu Apr 13, 2022

vlstill Apr 14, 2022

mihaibudiu Apr 13, 2022

vlstill Apr 14, 2022

fruffy commented Apr 13, 2022

vlstill commented Apr 14, 2022 •

edited

Loading

vlstill commented Apr 14, 2022

fruffy commented Apr 14, 2022

vlstill commented Apr 14, 2022

mihaibudiu Apr 15, 2022

vlstill Apr 19, 2022

mihaibudiu Apr 19, 2022

vlstill Apr 20, 2022

mihaibudiu Apr 15, 2022

vlstill Apr 19, 2022

mihaibudiu commented Apr 15, 2022

Fix expansion of signed ranges to masks #3212

Fix expansion of signed ranges to masks #3212

Conversation

vlstill commented Apr 13, 2022

jafingerhut left a comment

Choose a reason for hiding this comment

jafingerhut commented Apr 13, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fruffy commented Apr 13, 2022

vlstill commented Apr 14, 2022 • edited Loading

vlstill commented Apr 14, 2022

fruffy commented Apr 14, 2022

vlstill commented Apr 14, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mihaibudiu commented Apr 15, 2022

vlstill commented Apr 14, 2022 •

edited

Loading