Synthesizing optimal 8051 code with an SMT solver (2020)(lab.whitequark.org)
lab.whitequark.org
Synthesizing optimal 8051 code with an SMT solver (2020)
https://lab.whitequark.org/notes/2020-04-06/synthesizing-optimal-8051-code/
9 comments
I would love to see more practical applications of SMT, particularly as intros to newbies.
Check out angr [1], a symbolic execution engine, and claripy [2], its frontend to SMT solvers like z3. Depending on your background, I probably wouldn't describe angr as "for newbies," but claripy is a very clean SMT interface!
[1] https://angr.io
[2] https://api.angr.io/claripy.html
[1] https://angr.io
[2] https://api.angr.io/claripy.html
The (freely available) book "SAT/SMT by Example" [1] shows how a lot of different problems can be tackled with an SMT solver. I highly recommend it!
[1] https://sat-smt.codes/
[1] https://sat-smt.codes/
How wrote something here: https://savannah.gnu.org/forum/forum.php?forum_id=9203
to find struct layouts for a binary format. Reverse engineering DWG
to find struct layouts for a binary format. Reverse engineering DWG
That was my thought too. The author says that the memory usage grows extremely quickly; I wonder if there's a way to reduce it.
Having written way to much 8051 assembly I approve of this solution ....
It is great to see SMT used for more real problems though!