Cleaner handling of step limit

[Stevendeo]

This PR aims at cleanly stop when the step limit is reached instead of returning a Fatal Error

[hra687261]

LGTM modulo a couple of superficial suggestions

[hra687261]

Suggestion:

          | Errors.Run_error _ -> 
            returned_status := Worker_interface.Error "Run error"

[bclement-ocp]

I approved but actually — please add a test with a very low step limit (e.g. 1) and (get-info :reason-unknown) to ensure that:

• We properly return unknown when reaching the step lmit, and
• We properly say that the reason is due to the step limit

[bclement-ocp]

I don't think we can do this this way (see also #946 )

For satML in particular we would need to make sure that whenever the "step limit reached" exception is raised it cannot leave the solver in an invalid intermediate state, which we will very probably mess up. I have made comments on that fact wrt push but I now realize that it applies more generally — the sat solver was written with the fact that it could get interrupted by an exception at any time and then re-used. Trying to make it do so is probably a recipe for many bugs ranging from crashes to soundness holes.

Fixing this properly would be a huge amount of extremely error-prone work and frankly I don't think that it is worth it. I'd be in favor of simply putting the solver in a "imited" state once the steps limit (or time limit, for that matter) is exhausted, and make it reject all commands except for diagnostic ones (e.g. get-info). This would fix #934 without an equivalent implicit requirement (you really shouldn't keep using the solver once the steps limit has been exceeded because its output can be complete garbage at that point).

[bclement-ocp]

I this is raised by Steps.set_steps_bound the try .. with .. block should only include Steps.set_steps_bound here.

[Stevendeo]

If set_steps_bound fails, we do not want State.set to be called. It was written initially when I put "recoverable_error" instead of "fatal_error" in the next line.

[bclement-ocp]

In that case, the best way to write the code in modern OCaml is to use match .. exception:

match Steps.set_steps_bound i with
| () -> State.set steps_bound i st
| exception Invalid_argument _ ->
  fatal_error "..."

This helps controlling the scope of exception handling (I make the remark here because for standard exceptions such as Not_found, Failure, or Invalid_argument it is very easy to include an unrelated function in the try .. with .. block that could also raise that same exception and cause puzzling bugs).

[bclement-ocp]

@hra687261's suggestion of removing the match here still applies.

[bclement-ocp]

Can you explain why the steps limit increases while pushing? We call: E.fresh_name, save_guard_and_refs (which only pushes things on a stack), mk_gf (which is just a dumb record constructor) and ME.add, none of which seem to increase the step count.

[Stevendeo]

I thought fun_sat and satml_frontend had the same behavior regarding the steps; I was wrong.

[bclement-ocp]

Returning env here is not correct for satML. Because the underlying satml solver uses mutability, it is shared between env and acc; if we reach the steps limit here, new_vars (called through create_guard) can leave the satml solver in an inconsistent state with variables partially added. Plus, env will be out of sync with the content of the satml solver and weird things will follow.

I see two solutions here — either we make sure that new_vars returns a valid environment here, so that acc is correct in the exception handler and we can then pop a corresponding amount, or we temporarily disable the step limit while pushing. I'd prefer the second option (even though it can cause going slightly over the step limit) because the first one is opening up a can of worms where we will mess up and introduce subtle bugs in the future.

[Stevendeo]

Returning env here is not correct for satML.

That's the point of the TODO, we need to actually cancel the push instead of just returning the env. But disabling the step limit is a better idea, I'll go for it.

[bclement-ocp]

What I mean by "not correct" here is worse — it will cause the type of crashes that we see in #946 , see my toplevel comment.

[bclement-ocp]

you really shouldn't keep using the solver once the steps limit has been exceeded because its output can be complete garbage at that point

Note that this really only applies to satML, not to the Tableaux solver, since the Tableaux solver is purely functional and won't get stuck in an intermediate invalid state. But satML is the default solver that 99% of users will use, so…

[bclement-ocp]

Note that this really only applies to satML, not to the Tableaux solver, since the Tableaux solver is purely functional and won't get stuck in an intermediate invalid state. But satML is the default solver that 99% of users will use, so…

Well and even then only "pure" Tableaux, not Tableaux-CDCL, which has an internal CDCL solver that could potentially end up in an invalid state as well!

[Stevendeo]

Just in case, I disactivated the steps exception at the Frontend level to make sure we never break any invariant in the future.

[bclement-ocp]

Why not directly call Steps.apply_without_step_limit from inside Satml_frontend.push?

[Stevendeo]

Just in case, I disactivated the steps exception at the Frontend level to make sure we never break any invariant in the future.

For this reason

[bclement-ocp]

Same as above

[Stevendeo]

By blocking the instructions at the frontend level, we ensure the environment cannot be used in a wrong way. Besides, we may want to display information from the invalid environment when the step limit is reached, so I would rather keep it like that.

[bclement-ocp]

But if Step_limit_reached was raised, the env is potentially invalid to use. How do you avoid it being reused in this case?

[bclement-ocp]

These also need wrap_f

[Stevendeo]

I did not put the wrapper on these because I did not want to silently fail (fail = do nothing) on push and pop.

[bclement-ocp]

Ah, I did not catch this, but the wrapper should not silently fail, it should return an error.

If the underlying state of the SAT solver is invalid, there is no guarantee that push and pop are correct either, so this could possibly crash as well.

[Stevendeo]

Not now push can no longer fail with the disabled steps check

[Stevendeo]

Oh I see your point sorry, we may push a wrong environment; but is it really an issue?

[bclement-ocp]

Oh I see your point sorry, we may push a wrong environment; but is it really an issue?

If a step limit is reached, there may or may not be some invariants in the environment that are broken. Without looking at the code, I don't know which invariants are broken, or how calling push or pop interacts with those broken invariants. It might be that this is perfectly fine, it might not be, but we won't know without tracking all the invariants that can potentially get broken, and even then if we can only call push and pop it is not very interesting, so we should just prevent that.

[Stevendeo]

The sat environment should keep track of its own inconsistency wrt the steps; with this, we could actually save invalid environments, update the step number and make sure we don't ever work with invalid environments. What do you think?

[Stevendeo]

Nevermind, it's pretty much what is already done. When the unknown_reason is Some (Step_limit _) we should not be able to do anything

[bclement-ocp]

I am not sure I understand why updating the step number seems to be such a huge issue. Once we have an unknown reason with Step_limit updating the step number is not going to change that unknown reason. What am I missing here?

[Stevendeo]

Now we use the Limit step as a reason not to keep using the environment, it is not an issue anymore.

[bclement-ocp]

I believe that this is still leaking a potentially invalid environment into the wild without protecting it with an unknown reason. This should raise i_dont_know and it should be caught in handle_sat_exn in the frontend to set the state there to `Unknown and following operations will be protected by wrap_f.

[Stevendeo]

If we raise I_dont_know we will answer unknown during an assertion; is that really what we want to do? I would rather update the environment with the correct unknown_reason

[bclement-ocp]

If we raise I_dont_know we will answer unknown during an assertion

If we raise I_dont_know I think it should be caught by the frontend which will update the unknown reason as needed, and only display unknown once the solving loop is done processing, but worth checking.

[Stevendeo]

The unknown reason is on the sat solver side

[bclement-ocp]

Ah right — yeah returning the env with Step_limit unknown reason is what needs to happen then.

[bclement-ocp]

There are still some issues with the smt interface, see inline comments.

I wonder if we should call the option steps-bound. I know that this is the name of the CLI flag, but we use "limit" for the time limit and the Fourier-Motzkin cross-limit (not sure what that limits) and "limit" is closer to what it actually do. The other place we use "bound" is for the "age bound" that controls the behavior of matching and is not a resource limit. If we change the name, it should also be changed for the CLI options, so best to keep "steps-bound" for now and do the rename everywhere in a separate PR.

[bclement-ocp]

(Waiting for the benches currently running on next to merge)