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

Incorrect parse of Alt-Ergo reals #145

Closed
bclement-ocp opened this issue Apr 27, 2023 · 0 comments · Fixed by #148
Closed

Incorrect parse of Alt-Ergo reals #145

bclement-ocp opened this issue Apr 27, 2023 · 0 comments · Fixed by #148
Assignees
@bclement-ocp
Labels
bug

Comments

@bclement-ocp
Copy link
Contributor

Consider the following:

$ cat real.ae
goal g: 0.0 < 0xFFFFFF.0p104

This is valid using Alt-Ergo's legacy parser:

$ alt-ergo --frontend legacy real.ae
File "real.ae", line 1, characters 9-29: Valid (0.0002) (0 steps) (goal g)

But dolmen barfs:

$ alt-ergo --frontend dolmen real.ae
File "real.ae", line 1, character 14-28:
1 | goal g: 0.0 < 0xFFFFFF.0p104
                  ^^^^^^^^^^^^^^
Error Unbound identifier: `0xFFFFFF.0p104`

(Note: 0xFFFFFF.0p104 is 0xFFFFFF x 2^104 = 340282346638528859811704183484516925440)
@Gbury Gbury added the bug label Apr 27, 2023
bclement-ocp added a commit to bclement-ocp/dolmen that referenced this issue Apr 28, 2023
@bclement-ocp
Support hexadecimal reals in Alt-Ergo syntax
d2a9f25 
Alt-Ergo allows specifying real literals using hexadecimal notation.
For instance, [0x1.1p1] represents [(1 + 1/16) * 2^1 = 17/8].

Currently, dolmen parses such literals but does not typecheck them
properly.  This patch changes that.

Note that such reals are stored in [Builtins.Decimal] using their raw
representation. The documentation of [Builtins.Decimal] is updated to
indicate that fact, and to suggest evaluating the string within using
[Q.of_string] if canonicalization is required.

Fixes Gbury#145
@bclement-ocp bclement-ocp mentioned this issue Apr 28, 2023
Merged
bclement-ocp added a commit to bclement-ocp/dolmen that referenced this issue May 3, 2023
@bclement-ocp
Support hexadecimal reals in Alt-Ergo syntax
07bf316 
Alt-Ergo allows specifying real literals using hexadecimal notation.
For instance, [0x1.1p1] represents [(1 + 1/16) * 2^1 = 17/8].

Currently, dolmen parses such literals but does not typecheck them
properly.  This patch changes that.

Note that such reals are stored in [Builtins.Decimal] using their raw
representation. The documentation of [Builtins.Decimal] is updated to
indicate that fact, and to suggest evaluating the string within using
[Q.of_string] if canonicalization is required.

Fixes Gbury#145
@Gbury Gbury closed this as completed in #148 May 3, 2023
Gbury pushed a commit that referenced this issue May 3, 2023
@bclement-ocp
Support hexadecimal reals in Alt-Ergo syntax (#148)
6568923 
* Support hexadecimal reals in Alt-Ergo syntax

Alt-Ergo allows specifying real literals using hexadecimal notation.
For instance, [0x1.1p1] represents [(1 + 1/16) * 2^1 = 17/8].

Currently, dolmen parses such literals but does not typecheck them
properly.  This patch changes that.

Note that such reals are stored in [Builtins.Decimal] using their raw
representation. The documentation of [Builtins.Decimal] is updated to
indicate that fact, and to suggest evaluating the string within using
[Q.of_string] if canonicalization is required.

Fixes #145

* Add hexfloats to changelog
@Gbury Gbury mentioned this issue Jul 4, 2023
Merged
Gbury added a commit to Gbury/opam-repository that referenced this issue Jul 4, 2023
@Gbury
[new release] dolmen_type, dolmen_model, dolmen_lsp, dolmen_loop, dol…
a5d053e 
…men_bin and dolmen (0.9)

CHANGES:

### Doc

- Add examples in the doc and tuto for type-checking (including
  a minimal working example in the tutorial).

### UI

- Make the unknown logic fatal by default, and simply enabled
  in non-strict mode (PR#158)
- Add the `--check-flow` option to checks coherence of sequences
  of statements (PR#135)
- Ensure stability of error codes for the `dolmen` binary

### Parsing

- Add `attrs` fields for all declarations and definition types,
  and correctly attach predicate attribute to individual definitions
  (PR#130)
- Restore support for toplevel "and" in non-recursive predicate/function
  definitions in Alt-Ergo syntax (PR Gbury/dolmen#147, fixes issue Gbury/dolmen#144)
- Add support for hexadecimal floats in Alt-Ergo syntax (PR Gbury/dolmen#148, fixes
  issue Gbury/dolmen#145)
- Add local goals to the `Prove` statement (PR#140)
- Add a check-sat/prove-sat statement to ae's language (PR#140)

### Typing

- Ignore arithmetic restrictions when typing model values. This
  particularly affects difference logic (PR#141)
- Rename theory-specific configuration to `config` (instead of
  `arith`, `arrays`, etc..) (PR#142)
- Add printing function for logics (PR#142)
- Attach type definitions to type-defs (PR#157)
- Add a proper reason for reserved builtins (PR#155)
- Add bitvector builtins for alt-ergo's language (PR#136)

### Loop

- Add possibility for users of the loop library to choose the
  exit/return code for a `Code.t` (PR#134)
- Add the `Flow` module for flow checking (PR#135)
- Add the `check` function in `typer.ml`/`typer_intf.ml`
- Add `update` and `update_opt` in `State` (PR#156)
- Print type definitions in the printer of typed statements (PR#157)
- Prelude statements have been removed and replaced with prelude files (PR#160)
- `Typer.additional_builtins` is now a `State.key` and takes the current state
  and language as arguments (PR#160)

### Model

- Fix bug in bitvector implementation: negative inputs to `bvsmod`
  would raise an internal error (PR#138)
- Remove the "error" keyword and statement from smtlib2
  response (model) files (PR#139)
- Correctly compare abstract array values (PR#143)
- Accept extensions of functions/symbols with only partially defined
  semantics, for e.g. `fp.to_ubv`, `div`, etc.. (PR#151)
- Error out on incremental problems (PR#169)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@bclement-ocp bclement-ocp

Labels
bug
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Support hexadecimal reals in Alt-Ergo syntax bclement-ocp/dolmen
2 participants
@Gbury @bclement-ocp