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.

Sign up for GitHub

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

Jump to bottom

[Bug] [kompile] - Bison parser for Bytes in BYTES-SYNTAX is incorrect #2469

Closed
JKTKops opened this issue Mar 7, 2022 · 1 comment · Fixed by #2620
Closed

[Bug] [kompile] - Bison parser for Bytes in BYTES-SYNTAX is incorrect #2469

JKTKops opened this issue Mar 7, 2022 · 1 comment · Fixed by #2620
Assignees
@gtrepta
Labels
bug

Comments

@JKTKops
Copy link

JKTKops commented Mar 7, 2022 •
edited
Loading

K Version

$ kompile --version
K version:    5.2.94
Build date:   Fri Feb 25 08:26:57 CST 2022

Description

Generating a bison parser for the Bytes sort in the BYTES-SYNTAX module produces an incorrect parser.

$ kast --gen-parser -s Bytes -m BYTES-SYNTAX parser_Bytes
$ echo 'b"\x00\x00"' > bytes
$ ./parser_Bytes bytes
\dv{SortBytes{}}("b\"\\xf0\"")

The output should be \dv{SortBytes{}}("\xf0"). The extra quotes and escaping cause the Byte array, when consumed, to start with byte 0x42 (ASCII 'b') and continue with an ASCII quote etc. instead of containing the single byte 0xf0.

Input Files

module TEST
    imports BYTES
    configuration <k> $PGM:Bytes </k>
endmodule

module TEST-SYNTAX
    imports BYTES-SYNTAX
endmodule

Reproduction Steps / Expected Behavior

See description.
@JKTKops JKTKops added the bug label Mar 7, 2022
@dwightguth
Copy link
Collaborator

I'm fairly sure we have a special case in the bison parser for the String sort. We just need to modify the code to do something very similar with Bytes also.

@gtrepta gtrepta mentioned this issue May 24, 2022
Merged
@gtrepta gtrepta self-assigned this May 24, 2022
h0nzZik pushed a commit to h0nzZik/k that referenced this issue Nov 24, 2022
@rv-jenkins @ana-pantilie @ttuegel
Update dependency: haskell-backend/src/main/native/haskell-backend (r…
4497600 
…untimeverification#1830)

* haskell-backend/src/main/native/haskell-backend: 79703e11 - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: 8428df45 - LTS Haskell 17.4

* haskell-backend/src/main/native/haskell-backend: 2e714c56 - Add an EquationVariableName to RewritingVariableName

* haskell-backend/src/main/native/haskell-backend: c5cc46be - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: 0c4ad203 - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: a182994f - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: 9460590a - Simplify side conditions (runtimeverification#2393)

* haskell-backend/src/main/native/haskell-backend: 4fb83523 - Fix `variable` to `RewritingVariableName` in `Kore.Equation.Application` (runtimeverification#2325)

* haskell-backend/src/main/native/haskell-backend: f41cba23 - Revert "Revert runtimeverification#2315 (runtimeverification#2385)" (runtimeverification#2389)

* haskell-backend/src/main/native/haskell-backend: 44eed8d7 - Run Test workflow on macOS (runtimeverification#2420)

* haskell-backend/src/main/native/haskell-backend: 904f5322 - kore-repl: Print human-readable error messages (runtimeverification#2441)

* haskell-backend/src/main/native/haskell-backend: b49fdd3c - Make Conditional's term a strict field (runtimeverification#2442)

* haskell-backend/src/main/native/haskell-backend: 01f0402d - adding match for And (runtimeverification#2435)

* haskell-backend/src/main/native/haskell-backend: 3243d1e5 - kore-0.41.0.0 (runtimeverification#2444)

* haskell-backend/src/main/native/haskell-backend: 28913344 - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: abf0292b - Use unit and element symbol attributes

* haskell-backend/src/main/native/haskell-backend: 7d3ee1bc - Inefficient Equation renaming (runtimeverification#2438)

* haskell-backend/src/main/native/haskell-backend: 95b6c107 - Stop simplifying the left-hand side of equations (runtimeverification#2392)

* haskell-backend/src/main/native/haskell-backend: 21959d95 - Add instructions for running one test in Docker (runtimeverification#2456)

* haskell-backend/src/main/native/haskell-backend: 4195d948 - Removes sort checks for Map and Set during internalization (runtimeverification#2440)

* Predicates in the condition are now simplified

* haskell-backend/src/main/native/haskell-backend: c35bfa56 - Remove defined marker (runtimeverification#2380)

* haskell-backend/src/main/native/haskell-backend: 57ad3292 - Remove cabal.project.freeze (runtimeverification#2450)

* haskell-backend/src/main/native/haskell-backend: 66158c67 - Support the --bug-report and --no-bug-report options in kore-repl (#2462)

* haskell-backend/src/main/native/haskell-backend: f0d93ac5 - Use stderr for errors (runtimeverification#2458)

* haskell-backend/src/main/native/haskell-backend: 0427fae7 - Distinguish \bottom from stuck states (runtimeverification#2451)

* haskell-backend/src/main/native/haskell-backend: d136446e - Fix Strict performance (runtimeverification#2447)

* haskell-backend/src/main/native/haskell-backend: a4e55b2a - Remove IMP fragment tests (runtimeverification#2467)

* haskell-backend/src/main/native/haskell-backend: 1f61e5a6 - Revert PRs related to InternalAc, Unit, Element & Concat symbols changes (runtimeverification#2463)

* haskell-backend/src/main/native/haskell-backend: fcfc2d52 - Remove the EvaluatedF marker from TermLike (runtimeverification#2469)

* haskell-backend/src/main/native/haskell-backend: fb56d719 - Revert PR runtimeverification#2334 (runtimeverification#2473)

* haskell-backend/src/main/native/haskell-backend: bb258f14 - Add ref = "main"; to default.nix (runtimeverification#2475)

* haskell-backend/src/main/native/haskell-backend: 964e64e7 - Update dependency: deps/k_release (runtimeverification#2464)

* haskell-backend/src/main/native/haskell-backend: abf14770 - Emit a warning when kore-exec exceeds the depth limit (runtimeverification#2461)

* haskell-backend/src/main/native/haskell-backend: 003a8424 - Update dependency: deps/k_release (runtimeverification#2478)

* haskell-backend/src/main/native/haskell-backend: 485bd89a - kore-0.42.0.0 (runtimeverification#2477)

* Add definedness to lookup rules, regenerate tests

* haskell-backend/src/main/native/haskell-backend: 78515d10 - Update dependency: deps/k_release (runtimeverification#2486)

* Revert changes to domains.md and test output

* haskell-backend/src/main/native/haskell-backend: 4f3a751c - Format code with fourmolu (runtimeverification#2382)

* haskell-backend/src/main/native/haskell-backend: de80594b - Update dependency: deps/k_release (runtimeverification#2490)

* Update map symbolic Haskell tests

* haskell-backend/src/main/native/haskell-backend: 9c9ef914 - Update dependency: deps/k_release (runtimeverification#2495)

Co-authored-by: ana-pantilie <[email protected]>
Co-authored-by: Thomas Tuegel <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@gtrepta gtrepta

Labels
bug
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Correct the generated bison parser for Bytes runtimeverification/k
3 participants
@dwightguth @JKTKops @gtrepta