GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
437 stars 63 forks source link

Typechecker gap with record argument types #2105

Open sauclovian-g opened 3 weeks ago

sauclovian-g commented 3 weeks ago

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.

RyanGlScott commented 2 weeks ago

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