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

Map representation for record types #706

Closed
robdockins opened this issue Apr 17, 2020 · 7 comments · Fixed by #786
Closed

Map representation for record types #706

robdockins opened this issue Apr 17, 2020 · 7 comments · Fixed by #786
Assignees
@robdockins
Labels
tech-debt For issues that require some internal refactoring.
Milestone
2.9.0

Comments

@robdockins
Copy link
Contributor

We've had several bugs relating to non-normalized field order for record types (#702, #667); I'm pretty sure this isn't a comprehensive list.

We should probably fix this problem once-and-for-all by making sure all the intermediate type and value datatypes from typechecking onward use a Map or some other datastructure that enforces canonical ordering.
@robdockins robdockins added the tech-debt For issues that require some internal refactoring. label Apr 17, 2020
@brianhuffman
Copy link
Contributor

I think we should treat field name ordering in the same way that the MacOS filesystem treats case: It should be order-insensitive, yet order-preserving. For example, if I ask for the type of {b = 0x04, a = True}, I would expect to see { b : [8], a : Bit}, and not {a : Bit, b : [8]}.

So we might want to switch to using a Map in some places, but for Cryptol types at least, I think we should keep the list-based representation.

To avoid the kind of programming errors we've been seeing, perhaps we should introduce a new type for order-preserving, order-insensitive maps; it could be implemented as a newtype wrapper around [(Ident, a)].

@robdockins
Copy link
Contributor Author

We're currently being pretty inconsistent about this, so some sort of system for handling it would be good.

Perhaps a map structure together with a list indicating the "display order" of the fields would accomplish what we want.

@brianhuffman
Copy link
Contributor

Yes, that would be another way to implement it. We should wrap it up in a new abstract datatype so that we don't have to care how it's implemented.

@robdockins robdockins mentioned this issue Apr 18, 2020
Merged
@brianhuffman
Copy link
Contributor

In a comment on #703, I mentioned that I would like for :sat counterexamples to be shown with the record fields in the same order that I specified on the command line; we should fix that and add it as a regression test.

@atomb atomb added this to the 2.9.0 milestone May 5, 2020
@brianhuffman brianhuffman self-assigned this May 5, 2020
@robdockins
Copy link
Contributor Author

@brianhuffman, are you still planning to work on this soon?

@brianhuffman
Copy link
Contributor

It kind of fell off my radar; my top priority right now is the remaining soundness issues in saw-script. If you want to work on it now, you won't be stepping on my toes.

@robdockins
Copy link
Contributor Author

robdockins commented Jun 26, 2020 •
edited
Loading

Here is an exciting interaction I discovered. Apparently we haven't been checking for duplicate fields. I'm going to declare that this is a Bad Thing and remove this behavior as part of fixing this ticket.

Loading module Cryptol
Cryptol> let r = { f = 0x11, f = "asdf" }
Cryptol> :t r
r : {f : [8], f : [4][8]}
Cryptol> r.f
0x11
Cryptol> let r = { f = "asdf", f = 0x11 }
Cryptol> :t r
r : {f : [4][8], f : [8]}
Cryptol> r.f
[0x61, 0x73, 0x64, 0x66]

robdockins added a commit that referenced this issue Jun 26, 2020
@robdockins
Implement and use a new RecordMap type.
36e1e10 
This type stores records as a finite map from field names to
values, while also remembering the original order of the fields
from when the record was generated (usually, from the program source).
For all "semantic" purposes, the fields are treated as appearing in
a canoical order (in sorted order of the field names).  However, for
user display purposes, records are presented in the order in which
the fields were originally stated.

In the course of implementing this, I discovered that we were not
previously checking for repeated fields in the parser or typechecker,
which would result in some rather strange situations and could probably
be used to break the type safety. This is now fixed and repeated fields
will result in either a parse error or a panic (for records generated
internally).

Fixes #706
@robdockins robdockins mentioned this issue Jun 26, 2020
Merged
robdockins added a commit that referenced this issue Jun 30, 2020
@robdockins
Implement and use a new RecordMap type.
a52fcdd 
This type stores records as a finite map from field names to
values, while also remembering the original order of the fields
from when the record was generated (usually, from the program source).
For all "semantic" purposes, the fields are treated as appearing in
a canoical order (in sorted order of the field names).  However, for
user display purposes, records are presented in the order in which
the fields were originally stated.

In the course of implementing this, I discovered that we were not
previously checking for repeated fields in the parser or typechecker,
which would result in some rather strange situations and could probably
be used to break the type safety. This is now fixed and repeated fields
will result in either a parse error or a panic (for records generated
internally).

Fixes #706
robdockins added a commit that referenced this issue Jun 30, 2020
@robdockins
Implement and use a new RecordMap type.
6c6cb94 
This type stores records as a finite map from field names to
values, while also remembering the original order of the fields
from when the record was generated (usually, from the program source).
For all "semantic" purposes, the fields are treated as appearing in
a canoical order (in sorted order of the field names).  However, for
user display purposes, records are presented in the order in which
the fields were originally stated.

In the course of implementing this, I discovered that we were not
previously checking for repeated fields in the parser or typechecker,
which would result in some rather strange situations and could probably
be used to break the type safety. This is now fixed and repeated fields
will result in either a parse error or a panic (for records generated
internally).

Fixes #706
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@robdockins robdockins

Labels
tech-debt For issues that require some internal refactoring.
Projects
None yet
Milestone
2.9.0
Development

Successfully merging a pull request may close this issue.

Implement and use a new RecordMap type GaloisInc/cryptol
3 participants
@atomb @brianhuffman @robdockins