Add SMTZilla training scripts by hra687261 · Pull Request #542 · formalsec/smtml

hra687261 · 2026-02-16T16:22:12Z

This PR is rebased on #540 and should be merged after it. I created a separate PR to make reviewing easier.
This needs a bit more testing, which I will do later and then mark it as ready for review.
I notably don't know if using dune-site for this is overkill, but afaik that's the right/safe way to do it.

Note: The python code is a reimplementation of code originally written by @felixL-K

hra687261 · 2026-02-18T14:57:02Z

In fact it should be ready for a review. The only annoying thing is that dune-site seems to require dune build to work (dune exec alone does not suffice), which is not ideal, but I don't know if there is a way to fix that.

EDIT: The z3 CI failure is unrelated to this PR AFAIK.

filipeom

In fact it should be ready for a review. The only annoying thing is that dune-site seems to require dune build to work (dune exec alone does not suffice), which is not ideal, but I don't know if there is a way to fix that.

Yeah you have to at least do dune build @install before running dune exec. Not exactly sure why this happens but I'm used to it in ECMA-SL and other places where I've used dune-site.

EDIT: The z3 CI failure is unrelated to this PR AFAIK.

This one is annoying, seems something is turning on backtraces. Can you let me check something? I'll approve afterwards

hra687261 · 2026-02-19T01:05:30Z

This one is annoying, seems something is turning on backtraces.

Yes, I am not sure what, but I think we had something of the kind in owi, where backtraces were turned on somehow even if we do not do it explicitly (cc @redianthus ), but it's probably not related to this one, because AFAIK this did not happen before this PR, right?

Can you let me check something? I'll approve afterwards

Of course! There is no rush.

redianthus · 2026-02-19T11:12:00Z

What is this file ‎misc/out1s.bin ? It seems unused. Do we really need to have it in the repository ?

redianthus · 2026-02-19T11:13:10Z

Yes, I am not sure what, but I think we had something of the kind in owi, where backtraces were turned on somehow even if we do not do it explicitly (cc @redianthus ), but it's probably not related to this one, because AFAIK this did not happen before this PR, right?

Yes, still an issue I think: OCamlPro/owi#455

hra687261 · 2026-02-19T13:01:35Z

What is this file ‎misc/out1s.bin ? It seems unused. Do we really need to have it in the repository ?

It's an example of a marshalled file of queries (but it should've been renamed ...).
It's purpose is to make it easy to test the model training code without having to rerun benchmarks to generate the file of marshalled queries.
I was planning on writing some documentation on how to use this stuff (though it is pretty simple), but I haven't gotten to it yet.

redianthus · 2026-02-19T13:17:39Z

It's an example of a marshalled file of queries (but it should've been renamed ...).

OK, so, maybe we can have a smaller one if it's only for illustration purpose? (16MB of marshaled data is a lot!)

Maybe we could avoid having a file at all and show how to generate it in the documentation ?

filipeom

I'm approving as I'm satisfied with the PR at this time. But there seems to be a couple of open issues for you to discuss.

I'll try to summarize these below:

#542 (comment): Removal of requirments.txt
#542 (comment): Review of python code
#542 (comment): Removal or reduction in size of: misc/out1s.bin
#542 (comment): Backtrace making CI fail

The only one that may actually block merging is point 4. But maybe we can promote the file for the time being. Alternatively, I can always bypass merge protection rules if we don't want to forget to investigate the issue.

hra687261 · 2026-02-21T19:21:33Z

Done for 1 and 3. I'll try to investigate 4 before merging, the code changes are not significant so it should not be hard to find the source, but it is pretty surprising.

filipeom · 2026-02-24T17:43:06Z

Done for 1 and 3. I'll try to investigate 4 before merging, the code changes are not significant so it should not be hard to find the source, but it is pretty surprising.

I've also been doing a bit of investigation myself. It seems that dune-site forces the linkall flag (see ocaml/dune@ddefc99). Which may transitively include a let () = Printexc.record_backtrace true from dune itself or other library?

filipeom · 2026-02-24T17:49:25Z

I'm happy to merge, knowing that this is a fundamental issue with dune-site. We can address it later, although I'm not sure if it introduces a performance overhead. Maybe we can follow-up on geneweb/geneweb#2473 to see if there is something better 😅

redianthus · 2026-02-24T20:26:14Z

Well spotted!

I'm wondering if the culprit is dolmen (and base which seems to be a transitive deps of dolmen) : https://github.com/Gbury/dolmen/blob/master/src/bin/options.ml#L394-L398

hra687261 · 2026-02-26T01:02:46Z

Thanks for the information @filipeom

I'm wondering if the culprit is dolmen (and base which seems to be a transitive deps of dolmen) :

I think dolmen was already used by smtml no? (Unless it is the dolmen binary itself that is now linked and which wasn't before).
Either way I don't know if whichever library activates the recording of backtraces does that intentionally, it might be something we can ask them to stop doing. I would assume there is a cost to always recording backtraces (likely a small one but still).

Otherwise, we could simply turn off backtraces by hand on our side? Though it would probably confuse anyone who uses smtml, but it can be on the binary side only. Or it can be command line option like -b to set it to true otherwise it stays at false? (EDIT: Something like: hra687261#1?)

I'm happy to merge

I still haven't had the time to look at the machine learning stuff, maybe the end of this week or next week (we should be able to get a review on it by next it). I don't have a strong opinion I am ok with merging a first version now or waiting a bit.

…s package

…ad of `Error (`Msg ...)`

…e with dune-site

…nd creation

filipeom · 2026-02-26T09:15:39Z

I think dolmen was already used by smtml no? (Unless it is the dolmen binary itself that is now linked and which wasn't before).

My understanding is that since Dolmen uses the Base/Core libraries, and these turn backtraces on by default, we transitively get backtraces due to linkall because all the code from Base/Core is linked in our lib/bin. I don't know if that is indeed the case, but I don't think we will suffer much from backtraces. We don't do any control flow with exceptions (I think). We can benchmark it to see if there is any impact, but it's not a blocker for me.

I still haven't had the time to look at the machine learning stuff, maybe the end of this week or next week (we should be able to get a review on it by next it). I don't have a strong opinion I am ok with merging a first version now or waiting a bit.

I'm also ok with merging this as is. It can be reviewed/imporoved later and it would make accepting changes in subsequent PRs easier.

hra687261 · 2026-02-26T11:43:03Z

I'm also ok with merging this as is. It can be reviewed/imporoved later and it would make accepting changes in subsequent PRs easier.

Alright then, I'll promote the test and merge!

filipeom · 2026-02-26T11:49:17Z

I'm also ok with merging this as is. It can be reviewed/imporoved later and it would make accepting changes in subsequent PRs easier.

Alright then, I'll promote the test and merge!

Great thanks! 😃

hra687261 force-pushed the smtzilla_training branch from 98635a3 to d7870e6 Compare February 17, 2026 11:43

hra687261 marked this pull request as ready for review February 18, 2026 14:57

hra687261 requested a review from a team as a code owner February 18, 2026 14:57

filipeom reviewed Feb 18, 2026

View reviewed changes

Comment thread dune-project Outdated