search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
437 stars 63 forks source link

Solver caching fails to cache vector counter examples on What4 based tactics #1965

Open bboston7 opened 11 months ago

bboston7 commented 11 months ago

When proving a goal that produces a vector counter example via the What4 backend, the solver cacher fails with an error:

sawscript> set_solver_cache_path "/tmp"
sawscript> prove w4 {{ \(x : [3][8]) -> x == [1, 2, 3] }}
[23:45:31.156] Solver cache insert failed:
TODO: compute vector type, or just store it
CallStack (from HasCallStack):
  error, called at src/Verifier/SAW/Simulator/What4.hs:1261:19 in saw-core-what4-0.2-inplace:Verifier.SAW.Simulator.What4
[23:45:31.156] Invalid: [x = [254, 2, 3]]

The error seems to come up with any of the what4 based tactics (such as w4_unint_z3). The caching works just fine with non-what4 backends, so I think this is technically a bug in Verifier.SAW.Simulator.What4, but the solver cacher is the only way I know of to trigger it.

This bug is not critical, as the error does not crash SAW.

RyanGlScott commented 10 months ago

Do you know what is causing this, @m-yac?

m-yac commented 10 months ago

Yes, sorry I forgot to update the issue after Brett and I chatted a few weeks ago.

As Brett mentioned, this is from a bug with saw-core-what4, not solver caching. Specifically, the VecLabel case of getLabelValues in Verifier.SAW.Simulator.What4 contains an error is that only ever evaluated during solver caching.

This error can be limited to only the case of empty vectors by copying over the VecLabel case of getLabelValues in Verifier.SAW.Simulator.SBV. (In the future perhaps we should merge these two files in some way, since there seems to be a lot of identical code across the two files. I'm guessing the getLabel functions once had the same TODO error message, but the case was partially fixed on the SBV side and never copied over to the What4 side.)

However we also realized that if solver caching encounters a error, it should not print the full message lest the user thinks something has actually gone wrong (whenever solver caching encounters an error, it falls back to just calling the solver directly). We were thinking instead the message should read:

[23:45:31.156] [Warning] Solver cache insert failed, falling back to calling solver (use -v Debug to see error)

and thus only show the full message if -v Debug is used.

When I get a chance I will make a PR for both changes.