Skip to content
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.

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

Heapster: Resolve shift/reduce conflict warnings in parser #1794

Closed
RyanGlScott opened this issue Jan 4, 2023 · 1 comment · Fixed by #1795
Closed

Heapster: Resolve shift/reduce conflict warnings in parser #1794

RyanGlScott opened this issue Jan 4, 2023 · 1 comment · Fixed by #1795
Assignees
Labels
subsystem: heapster Issues specifically related to memory verification using Heapster

Comments

@RyanGlScott
Copy link
Contributor

One unfortunate consequence of #1792 (which wasn't noticed until after it landed) is that it introduced a new warning when compiling Verifier.SAW.Heapster.CruUtil:

shift/reduce conflicts:  9

This is because of the new '-' expr production. To see where exactly the shift/reduce conflicts lie, you can run the following command:

$ cabal run happy -- -agc --strict heapster-saw/src/Verifier/SAW/Heapster/Parser.y -idetailed-info.txt

I've attached the generated detailed-info.txt file. The relevant bits are this at the top:

state 90 contains 9 shift/reduce conflicts.

Here is state 90:

State 90

    expr -> expr . '+' expr                             (rule 24)
    expr -> '-' expr .                                  (rule 25)
    expr -> expr . '*' expr                             (rule 26)
    expr -> expr . 'orsh' expr                          (rule 37)
    expr -> expr . ';' expr                             (rule 38)
    expr -> expr . 'or' expr                            (rule 49)
    expr -> expr . '==' expr                            (rule 60)
    expr -> expr . '/=' expr                            (rule 61)
    expr -> expr . '<u' expr                            (rule 62)
    expr -> expr . '<=u' expr                           (rule 63)

    ')'            reduce using rule 25
    ']'            reduce using rule 25
    '}'            reduce using rule 25
    '>'            reduce using rule 25
    ':'            reduce using rule 25
    ';'            shift, and enter state 98
            (reduce using rule 25)

    ','            reduce using rule 25
    '+'            shift, and enter state 99
            (reduce using rule 25)

    '*'            shift, and enter state 100
            (reduce using rule 25)

    '-o'           reduce using rule 25
    '=='           shift, and enter state 101
            (reduce using rule 25)

    '/='           shift, and enter state 102
            (reduce using rule 25)

    '<u'           shift, and enter state 103
            (reduce using rule 25)

    '<=u'          shift, and enter state 104
            (reduce using rule 25)

    'or'           shift, and enter state 105
            (reduce using rule 25)

    'orsh'         shift, and enter state 106
            (reduce using rule 25)

    %eof           reduce using rule 25

Where rule 25 is:

expr -> '-' . expr                                  (rule 25)

An example of the ambiguity is:

- 42 + 27

There are two possible ways to parse this:

  • Scenario A: (- 42) + 27
  • Scenario B: - (42 + 27)

How is this determined? At some point, the parser gets to the following state:

  • Parse stack: - 42
  • Next tokens: + 27 ...

Scenario A:

  1. REDUCE - 42 to exp:
    • Parse stack: exp
    • Next tokens: + 27 ...
  2. SHIFT:
    • Parse stack: exp +
    • Next tokens: 27 ...
  3. SHIFT:
    • Parse stack: exp + 27
    • Next tokens: ...
  4. REDUCE exp + 27 to exp:
    • Parse stack: exp
    • Next tokens: ...

Scenario B:

  1. SHIFT:
    • Parse stack: - 42 +
    • Next tokens: 27 ...
  2. SHIFT:
    • Parse stack: - 42 + 27
    • Next tokens: ...
  3. REDUCE 42 + 27 to exp:
    • Parse stack: - exp
    • Next tokens: ...
  4. REDUCE - exp to exp:
    • Parse stack: exp
    • Next tokens: ...

Whenever there is a shift/reduce conflict, happy defaults to shifting. As a result, happy picks Scenario B. This is arguably not what we want, as we would like - to bind more tightly than other operators.

One way to fix this would be to use happy's precedence pragmas. An example of how to do this can be found here.

@RyanGlScott RyanGlScott added the subsystem: heapster Issues specifically related to memory verification using Heapster label Jan 4, 2023
@RyanGlScott RyanGlScott self-assigned this Jan 4, 2023
@eddywestbrook
Copy link
Contributor

I agree that scenario A seems like the correct answer, and using precedence pragmas seem like a good way to affect this answer

RyanGlScott added a commit that referenced this issue Jan 4, 2023
We now ensure that `-` has higher precedence than any other operator using
`happy`'s `%left` pragma. This ensures that `- 42 + 27` parses as `(- 42) +
27`, not `- (42 + 27)` like before.

While I was in town, I added `%expect 0` at the top of the parser to ensure
that `happy` will error out in the future if additional shift/reduce conflicts
are introduced.

Fixes #1794.
@mergify mergify bot closed this as completed in #1795 Jan 4, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: heapster Issues specifically related to memory verification using Heapster
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants