Skip to content

Commit

Permalink
Heapster: Avoid shift/reduce conflicts involving bitvector negation
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
RyanGlScott committed Jan 4, 2023
1 parent 7a6c8e1 commit 1dcdee3
Showing 1 changed file with 6 additions and 1 deletion.
7 changes: 6 additions & 1 deletion heapster-saw/src/Verifier/SAW/Heapster/Parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,8 @@ import Verifier.SAW.Heapster.UntypedAST

}

%expect 0 -- shift/reduce conflicts

%tokentype { Located Token }
%token
'(' { Located $$ TOpenParen }
Expand Down Expand Up @@ -108,6 +110,7 @@ NAT { (traverse tokenNat -> Just $$) }
%left '+'
%left '*'
%nonassoc '@'
%left NEGPREC

%%

Expand Down Expand Up @@ -136,7 +139,9 @@ expr :: { AstExpr }
| NAT { ExNat (pos $1) (locThing $1) }
| 'unit' { ExUnit (pos $1) }
| expr '+' expr { ExAdd (pos $2) $1 $3 }
| '-' expr { ExNeg (pos $1) $2 }
-- NB: Give negation the highest possible precedence to avoid shift/reduce
-- conflicts with other operators, such as + and *.
| '-' expr %prec NEGPREC { ExNeg (pos $1) $2 }
| expr '*' expr { ExMul (pos $2) $1 $3 }
| 'struct' '(' list(expr) ')' { ExStruct (pos $1) $3 }
| lifetime 'array' '(' expr ',' expr ',' '<' expr ',' '*' expr ',' expr ')'
Expand Down

0 comments on commit 1dcdee3

Please sign in to comment.