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

Hide unsafe code from the optimiser #160

Merged
merged 2 commits into from
Sep 2, 2022
Merged

Hide unsafe code from the optimiser #160

merged 2 commits into from
Sep 2, 2022

Conversation

lthls
Copy link
Contributor

@lthls lthls commented Sep 1, 2022

The type definition for alternatives is a record, so a clever compiler (such as Flambda 2) can assume that values of this type can never be equal to 0. This translates all alts == noalts checks into trivial false constants, eventually breaking down with a segfault when noalts is actually passed.
My proposed fix is the minimal one: hide the constant 0 from the compiler, so it can't optimise away.
The real fix is to use a variant definition. Example:

and alternative =
| Noalts
| Alts of {
  cutto_alts : alternative;
  program : prolog_prog;
  adepth : int;
  agoal_hd : constant;
  ogoal_arg : term;
  ogoal_args : term list;
  agid : UUID.t; [@trace]
  goals : goal list;
  stack : frame;
  trail : T.trail;
  state : State.t;
  clauses : clause list;
  next : alternative;
}

It's exactly the same runtime representation as the current one, but type-safe.

@gares
Copy link
Contributor

gares commented Sep 1, 2022

I've already undone this optimization in #118, that that PR may need more months to complete.
Is Flambda 2 out?

@lthls
Copy link
Contributor Author

lthls commented Sep 1, 2022

No, Flambda 2 is not out yet, but it's in a good enough state that we're doing opam-wide testing. We can deal with packages failing with known issues, so it's not particularly urgent that you fix this issue.
If you plan a release before your other PR is merged, then including this patch would be nice as it would make our CI happy again, otherwise you can just ignore this.
We might actually fix it on our side by tweaking the implementation of Obj.magic anyway.

@gares
Copy link
Contributor

gares commented Sep 1, 2022

CI fails because I did not port here a fix to the opam package which was done in the opam repo.
I'm fine merging this, but I lack time, so if you could update the opam file here and make CI happy, that would be great.
I shall release before tabling is merged.

@gares gares merged commit d12a5ba into LPCIC:master Sep 2, 2022
@gares
Copy link
Contributor

gares commented Sep 2, 2022

Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants