OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

Fully disable heavy assertions #1089

Closed Halbaroth closed 5 months ago

Halbaroth commented 5 months ago

In some part of the codebase, we use heavy assertions as follow:

assert (not @@ Options.get_enable_assertions () || heavy_assertion)

This trick has two advantages:

This PR adds a new function in Options to reproduce this good design everywhere in the codebase.

Notice that I put the function heavy_assert in Options but it would be better to put it in Util. Alas, we got a cycle dependency :/

bclement-ocp commented 5 months ago

I'm OK with the idea (although my personal opinion is that there isn't much value in using no-assert), but I don't understand what Lazy.t brings to the equation? We don't share Lazy.t objects so I fail to see what it brings compared to unit -> 'a functions (I believe Lazy.force requires a synchronization point in OCaml 5).

* If we use the compiler option `no-asserts`, we don't even test the option `Options.get_enable_assertions`.

I believe (but did not check) that even without flambda, if Options.get_enable_assertions () then () else () should be eliminated (if get_enable_assertions is inlined) anyways.

Halbaroth commented 5 months ago

I believe (but did not check) that even without flambda, if Options.get_enable_assertions () then () else () should be eliminated (if get_enable_assertions is inlined) anyways.

Uhm maybe. In this case If Options.get_enable_assertions () then heavy_assert; is more readable than assert (not ... || ...).

I used a lazy value to reproduce the short circuit behavior of the logic operator or. If you write heavy_assert (your_condition), we can imagine that your_condition will be evaluate before calling heavy_assert.

EDIT: ok, I just want a suspension and I don't care to memoize the value. I just forgot lazy is more than lazy evaluation but demand evaluation.

bclement-ocp commented 5 months ago

I used a lazy value to reproduce the short circuit behavior of the logic operator or. If you write heavy_assert (your_condition), we can imagine that your_condition will be evaluate before calling heavy_assert.

I meant that we can write heavy_assert (fun () -> your_condition)

Halbaroth commented 5 months ago

I asked some gurus about the simplification of if cond then () else (). It seems that flambda 1 doesn't simplify it, but flambda 2 does.

Besides, our condition is actually a call to an impure function but we only read a reference and flambda 2 can simplify this case too.

bclement-ocp commented 5 months ago

I asked some gurus about the simplification of if cond then () else (). It seems that flambda 1 doesn't simplify it, but flambda 2 does.

Seems I keep forgetting how much OCaml doesn't optimize stuff (: