goose-lang / goose

Goose converts a small subset of Go to Coq
MIT License
103 stars 11 forks source link

Incorrect codegen for struct constructor with nil field #47

Open sanjit-bhat opened 8 months ago

sanjit-bhat commented 8 months ago
type S struct {
    s *uint64
}

func Bad() *S {
    return &S{s: nil}
}

gets translated into

Definition S := struct.decl [
  "s" :: ptrT
].

Definition Bad: val :=
  rec: "Bad" <> :=
    struct.new S [
      "s" ::= slice.nil
    ].

One bad thing that happens as a result is that the new struct fails val_ty because slice.nil is not a valid ptrT.

tchajed commented 8 months ago

This is because at least when we initially developed Goose the go/types package didn't help differentiate nil for a slice vs a pointer (it assigned them the same "untyped nil" type as far as I recall). It's possible to get type info from context, but the whole point of using go/types was to not do this kind of type inference work.

At least from following the release notes I don't believe this has changed, but it would be nice to encode this as a test case and check that it still holds.

For your particular example I believe letting s be initialized to its default value will use the type from the struct declaration, which will work correctly.