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

rec_check.ml: fix a bug in recursive class declarations check. #1915

Merged
merged 1 commit into from Jul 29, 2018

Conversation

Projects
None yet
4 participants
@Cemoixerestre
Copy link
Contributor

commented Jul 18, 2018

# class a = let x() = new a in let y = x() in object end;;
Warning 26: unused variable y.
Segmentation fault (core dumped)

@trefis trefis requested a review from yallop Jul 18, 2018

@yallop

This comment has been minimized.

Copy link
Member

commented Jul 18, 2018

I'll try to take a look at this next week.

@gasche gasche added the bug label Jul 18, 2018

@gasche

This comment has been minimized.

Copy link
Member

commented Jul 18, 2018

@yallop no problem, thanks for the notice.

Note: I think the fix, if approved, should go in the maintenance 4.07 branch -- the Changes entry is placed there.

@yallop

yallop approved these changes Jul 28, 2018

Copy link
Member

left a comment

There's one typo in a comment, but I'm otherwise happy.

@@ -716,8 +716,11 @@ let is_valid_class_expr idlist ce =
| Tcl_fun (_, _, _, _, _) -> Use.empty
| Tcl_apply (_, _) -> Use.empty
| Tcl_let (rec_flag, valbinds, _, ce) ->
let _, ty = value_bindings rec_flag env valbinds in
Use.join ty (class_expr env ce)
(* This rule looks like the `Texp_rule` in the expression function,

This comment has been minimized.

Copy link
@yallop

yallop Jul 28, 2018

Member

The comment should read "… like the Texp_let rule …"

Use.join ty (class_expr env ce)
(* This rule looks like the `Texp_rule` in the expression function,
but is more restrictive. Maybe we should add `Use.discard` to
make this rule more similar. *)

This comment has been minimized.

Copy link
@yallop

yallop Jul 28, 2018

Member

Maybe we should add Use.discardto make this rule more similar.

Since Use.discard won't perform any useful function here, I think it's best to leave it out.

Here's my reasoning for why Use.discard would do nothing: the only way to use a class name in a computation is via new, which counts as an inspection; inspection turns everything into dereferencing; any further surrounding contexts can only turn Dereferenced into Dereferenced or Guarded, both of which are left unchanged by guarded.

@gasche

This comment has been minimized.

Copy link
Member

commented Jul 28, 2018

Yes, I agree with the reasoning for why discard is a no-op here.

Thanks for the review! I will fix the typo and rebase the PR.

@gasche gasche force-pushed the Cemoixerestre:rec_class_bug branch from b977827 to 445593d Jul 28, 2018

@gasche

This comment has been minimized.

Copy link
Member

commented Jul 28, 2018

I rebased the PR, and added a precise comment on the lack of discard.

rec_check.ml: fix a bug in recursive class declarations check.
    # class a = let x() = new a in let y = x() in object end;;
    Warning 26: unused variable y.
    Segmentation fault (core dumped)

@gasche gasche merged commit 9e45a79 into ocaml:trunk Jul 29, 2018

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details

gasche added a commit that referenced this pull request Jul 29, 2018

Merge pull request #1915 from Cemoixerestre/rec_class_bug
rec_check.ml: fix a bug in recursive class declarations check.

(cherry picked from commit 9e45a79)

gasche added a commit that referenced this pull request Jul 29, 2018

@gasche

This comment has been minimized.

Copy link
Member

commented Jul 29, 2018

When I cherry-picked in 4.07 ( 8e043eb ) I realized that there are two occurrences of Tcl_let, one in the regular check and one in check_class_expr, using the same code -- our bug was only for the check_class_expr case. I decided to make the same change in the regular check, as I believe it is more correct (but it's possible that the Use.inspect around it would prevent a problem there). I just pushed a small commit to the same effect in trunk, 725c620.

gasche added a commit to gasche/ocaml that referenced this pull request Jul 30, 2018

Changes for the let-rec patchset + general commit-message explanation
This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

gasche added a commit to gasche/ocaml that referenced this pull request Jul 30, 2018

Changes for the let-rec patchset + general commit-message explanation
This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

gasche added a commit to gasche/ocaml that referenced this pull request Jul 30, 2018

Changes for the let-rec patchset + general commit-message explanation
This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

gasche added a commit to gasche/ocaml that referenced this pull request Jul 30, 2018

Changes for the let-rec patchset + general commit-message explanation
This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

gasche added a commit to gasche/ocaml that referenced this pull request Aug 9, 2018

Changes for the let-rec patchset + general commit-message explanation
This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

gasche added a commit to gasche/ocaml that referenced this pull request Aug 18, 2018

Changes for the let-rec patchset + general commit-message explanation
This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

gasche added a commit to gasche/ocaml that referenced this pull request Sep 2, 2018

Changes for the let-rec patchset + general commit-message explanation
This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)
        | Unused (* the value is not used at all *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

gasche added a commit to gasche/ocaml that referenced this pull request Sep 10, 2018

Changes for the let-rec patchset + general commit-message explanation
This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)
        | Unused (* the value is not used at all *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

gasche added a commit to gasche/ocaml that referenced this pull request Sep 13, 2018

Changes for the let-rec patchset + general commit-message explanation
This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)
        | Unused (* the value is not used at all *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.
@damiendoligez

This comment has been minimized.

Copy link
Member

commented Sep 18, 2018

@Cemoixerestre @yallop, any comment on @gasche's tweak described above?

@yallop

This comment has been minimized.

Copy link
Member

commented Sep 18, 2018

@damiendoligez: the tweak may be overzealous, but it appears to be harmless.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.