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.

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

Typechecker gap with record argument types #2105

Open
sauclovian-g opened this issue Aug 23, 2024 · 1 comment
Open

Typechecker gap with record argument types #2105

sauclovian-g opened this issue Aug 23, 2024 · 1 comment
Assignees
Labels
needs test Issues for which we should add a regression test tech debt Issues that document or involve technical debt topics: error-handling Issues involving the way SAW responds to an error condition topics: error-messages Issues involving the messages SAW produces on error type: bug Issues reporting bugs or unexpected/unwanted behavior unsoundness Issues that can lead to unsoundness or false verification

Comments

@sauclovian-g
Copy link
Collaborator

I do not think saw should accept this program, but it does:

typedef Stuff = {
   foo: Int,
   bar: String
};

let make (a: Int) (b: String) = { foo = a, baz = b };
let get (t: Stuff) = t.bar;
let go (a: Int) (b: String) = get (make a b);

If you add another line that invokes go, it appears that the typechecker accepts the program and then execution crashes somewhere further downstream:

typedef Stuff = {
   foo: Int,
   bar: String
};

let make (a: Int) (b: String) = { foo = a, baz = b };
let get (t: Stuff) = t.bar;
let go (a: Int) (b: String) = get (make a b);
let x = go 3 "abc";

which produces

no such record field: bar
CallStack (from HasCallStack):
  error, called at src/SAWScript/Value.hs:418:18 in saw-script-1.1.0.99-inplace:SAWScript.Value

If in this version you substitute "foo" for "bar" in get, it accepts it; if you substitute anything else, you get "Selecting a missing field" and no crash. In other words, the problem is that the invocation of get with a mismatched record type is accepted, and then the value of that record type doesn't have an entry for the requested field so access to it blows up later.

@sauclovian-g sauclovian-g self-assigned this Aug 23, 2024
@sauclovian-g sauclovian-g added type: bug Issues reporting bugs or unexpected/unwanted behavior topics: error-messages Issues involving the messages SAW produces on error tooling: test infrastructure Issues involving test infrastructure or test execution, or making SAW more testable unsoundness Issues that can lead to unsoundness or false verification tech debt Issues that document or involve technical debt topics: error-handling Issues involving the way SAW responds to an error condition labels Aug 23, 2024
@RyanGlScott
Copy link
Contributor

Ouch. Perhaps we need a "records" label, given how many odd issues we've uncovered with how records are implemented in SAWScript.

@sauclovian-g sauclovian-g added needs test Issues for which we should add a regression test and removed tooling: test infrastructure Issues involving test infrastructure or test execution, or making SAW more testable labels Oct 24, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
needs test Issues for which we should add a regression test tech debt Issues that document or involve technical debt topics: error-handling Issues involving the way SAW responds to an error condition topics: error-messages Issues involving the messages SAW produces on error type: bug Issues reporting bugs or unexpected/unwanted behavior unsoundness Issues that can lead to unsoundness or false verification
Projects
None yet
Development

No branches or pull requests

2 participants