From 1dcdee3afe02e0bbb2ae88be8d880ff815a77657 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 4 Jan 2023 15:36:34 -0600 Subject: [PATCH] Heapster: Avoid shift/reduce conflicts involving bitvector negation 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. --- heapster-saw/src/Verifier/SAW/Heapster/Parser.y | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Parser.y b/heapster-saw/src/Verifier/SAW/Heapster/Parser.y index 1bbe8d9639..5a93de1d8d 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Parser.y +++ b/heapster-saw/src/Verifier/SAW/Heapster/Parser.y @@ -22,6 +22,8 @@ import Verifier.SAW.Heapster.UntypedAST } +%expect 0 -- shift/reduce conflicts + %tokentype { Located Token } %token '(' { Located $$ TOpenParen } @@ -108,6 +110,7 @@ NAT { (traverse tokenNat -> Just $$) } %left '+' %left '*' %nonassoc '@' +%left NEGPREC %% @@ -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 ')'